Theorem infxpidmlem7 7509

Description: Lemma for infxpidm 7515. The union of a collection C of chains in H is a bijection.

Hypotheses

Ref	Expression
infxpidmlem.1	|- H = {f | (f = (/) \/ E.t((om ~<_ t /\ t (_ A) /\ f:(t X. t)-1-1-onto->t))}
infxpidmlem6.2	|- B = ran U. C

Assertion

Ref	Expression
infxpidmlem7	|- ((C (_ H /\ A.g e. C A.h e. C (g (_ h \/ h (_ g)) -> U.C:(B X. B)-1-1-onto->B)

Distinct variable groups:   f,g,h,t,A   B,f,g,h,t   C,f,g,h,t   g,H,h

Proof of Theorem infxpidmlem7

Step	Hyp	Ref	Expression
1		r19.26 1747	. . . . . . 7 |- (A.g e. C ((Fun g /\ Fun `'g) /\ A.h e. C (g (_ h \/ h (_ g)) <-> (A.g e. C (Fun g /\ Fun `'g) /\ A.g e. C A.h e. C (g (_ h \/ h (_ g)))
2		fun11uni 3557	. . . . . . 7 |- (A.g e. C ((Fun g /\ Fun `'g) /\ A.h e. C (g (_ h \/ h (_ g)) -> (Fun U.C /\ Fun `'U.C))
3	1, 2	sylbir 201	. . . . . 6 |- ((A.g e. C (Fun g /\ Fun `'g) /\ A.g e. C A.h e. C (g (_ h \/ h (_ g)) -> (Fun U.C /\ Fun `'U.C))
4		ssel 2059	. . . . . . . 8 |- (C (_ H -> (g e. C -> g e. H))
5		infxpidmlem.1	. . . . . . . . . 10 |- H = {f | (f = (/) \/ E.t((om ~<_ t /\ t (_ A) /\ f:(t X. t)-1-1-onto->t))}
6		visset 1809	. . . . . . . . . 10 |- g e. V
7	5, 6	infxpidmlem2 7504	. . . . . . . . 9 |- (g e. H <-> (g = (/) \/ E.x((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x)))
8		f10 3704	. . . . . . . . . . . 12 |- (/):(/)-1-1->(/)
9		f1eq1 3651	. . . . . . . . . . . 12 |- (g = (/) -> (g:(/)-1-1->(/) <-> (/):(/)-1-1->(/)))
10	8, 9	mpbiri 194	. . . . . . . . . . 11 |- (g = (/) -> g:(/)-1-1->(/))
11		df-f1 3190	. . . . . . . . . . . 12 |- (g:(/)-1-1->(/) <-> (g:(/)-->(/) /\ Fun `'g))
12		ffun 3621	. . . . . . . . . . . . 13 |- (g:(/)-->(/) -> Fun g)
13	12	anim1i 334	. . . . . . . . . . . 12 |- ((g:(/)-->(/) /\ Fun `'g) -> (Fun g /\ Fun `'g))
14	11, 13	sylbi 199	. . . . . . . . . . 11 |- (g:(/)-1-1->(/) -> (Fun g /\ Fun `'g))
15	10, 14	syl 10	. . . . . . . . . 10 |- (g = (/) -> (Fun g /\ Fun `'g))
16		f1of1 3679	. . . . . . . . . . . . 13 |- (g:(x X. x)-1-1-onto->x -> g:(x X. x)-1-1->x)
17		df-f1 3190	. . . . . . . . . . . . . 14 |- (g:(x X. x)-1-1->x <-> (g:(x X. x)-->x /\ Fun `'g))
18		ffun 3621	. . . . . . . . . . . . . . 15 |- (g:(x X. x)-->x -> Fun g)
19	18	anim1i 334	. . . . . . . . . . . . . 14 |- ((g:(x X. x)-->x /\ Fun `'g) -> (Fun g /\ Fun `'g))
20	17, 19	sylbi 199	. . . . . . . . . . . . 13 |- (g:(x X. x)-1-1->x -> (Fun g /\ Fun `'g))
21	16, 20	syl 10	. . . . . . . . . . . 12 |- (g:(x X. x)-1-1-onto->x -> (Fun g /\ Fun `'g))
22	21	adantl 388	. . . . . . . . . . 11 |- (((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) -> (Fun g /\ Fun `'g))
23	22	19.23aiv 1293	. . . . . . . . . 10 |- (E.x((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) -> (Fun g /\ Fun `'g))
24	15, 23	jaoi 341	. . . . . . . . 9 |- ((g = (/) \/ E.x((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x)) -> (Fun g /\ Fun `'g))
25	7, 24	sylbi 199	. . . . . . . 8 |- (g e. H -> (Fun g /\ Fun `'g))
26	4, 25	syl6 22	. . . . . . 7 |- (C (_ H -> (g e. C -> (Fun g /\ Fun `'g)))
27	26	r19.21aiv 1710	. . . . . 6 |- (C (_ H -> A.g e. C (Fun g /\ Fun `'g))
28	3, 27	sylan 448	. . . . 5 |- ((C (_ H /\ A.g e. C A.h e. C (g (_ h \/ h (_ g)) -> (Fun U.C /\ Fun `'U.C))
29		ssel2 2060	. . . . . . . . . . . . 13 |- ((C (_ H /\ g e. C) -> g e. H)
30	5	infxpidmlem4 7506	. . . . . . . . . . . . 13 |- (g e. H -> dom g = (ran g X. ran g))
31	29, 30	syl 10	. . . . . . . . . . . 12 |- ((C (_ H /\ g e. C) -> dom g = (ran g X. ran g))
32		ra4e 1692	. . . . . . . . . . . . . . . . 17 |- ((g e. C /\ y e. ran g) -> E.g e. C y e. ran g)
33		infxpidmlem6.2	. . . . . . . . . . . . . . . . . 18 |- B = ran U. C
34	5, 33	infxpidmlem6 7508	. . . . . . . . . . . . . . . . 17 |- (y e. B <-> E.g e. C y e. ran g)
35	32, 34	sylibr 200	. . . . . . . . . . . . . . . 16 |- ((g e. C /\ y e. ran g) -> y e. B)
36	35	ex 373	. . . . . . . . . . . . . . 15 |- (g e. C -> (y e. ran g -> y e. B))
37	36	ssrdv 2066	. . . . . . . . . . . . . 14 |- (g e. C -> ran g (_ B)
38		ssxp 3251	. . . . . . . . . . . . . . 15 |- ((ran g (_ B /\ ran g (_ B) -> (ran g X. ran g) (_ (B X. B))
39	38	anidms 434	. . . . . . . . . . . . . 14 |- (ran g (_ B -> (ran g X. ran g) (_ (B X. B))
40	37, 39	syl 10	. . . . . . . . . . . . 13 |- (g e. C -> (ran g X. ran g) (_ (B X. B))
41	40	adantl 388	. . . . . . . . . . . 12 |- ((C (_ H /\ g e. C) -> (ran g X. ran g) (_ (B X. B))
42	31, 41	eqsstrd 2091	. . . . . . . . . . 11 |- ((C (_ H /\ g e. C) -> dom g (_ (B X. B))
43	42	sseld 2063	. . . . . . . . . 10 |- ((C (_ H /\ g e. C) -> (y e. dom g -> y e. (B X. B)))
44	43	r19.23adva 1744	. . . . . . . . 9 |- (C (_ H -> (E.g e. C y e. dom g -> y e. (B X. B)))
45		dmuni 3314	. . . . . . . . . . 11 |- dom U. C = U_g e. C dom g
46	45	eleq2i 1535	. . . . . . . . . 10 |- (y e. dom U. C <-> y e. U_g e. C dom g)
47		eliun 2565	. . . . . . . . . 10 |- (y e. U_g e. C dom g <-> E.g e. C y e. dom g)
48	46, 47	bitr 173	. . . . . . . . 9 |- (y e. dom U. C <-> E.g e. C y e. dom g)
49	44, 48	syl5ib 206	. . . . . . . 8 |- (C (_ H -> (y e. dom U. C -> y e. (B X. B)))
50	49	ssrdv 2066	. . . . . . 7 |- (C (_ H -> dom U. C (_ (B X. B))
51	50	adantr 389	. . . . . 6 |- ((C (_ H /\ A.g e. C A.h e. C (g (_ h \/ h (_ g)) -> dom U. C (_ (B X. B))
52		relxp 3250	. . . . . . . 8 |- Rel (B X. B)
53	52	a1i 8	. . . . . . 7 |- ((C (_ H /\ A.g e. C A.h e. C (g (_ h \/ h (_ g)) -> Rel (B X. B))
54		sseq1 2078	. . . . . . . . . . . . . 14 |- (g = w -> (g (_ h <-> w (_ h))
55		sseq2 2079	. . . . . . . . . . . . . 14 |- (g = w -> (h (_ g <-> h (_ w))
56	54, 55	orbi12d 626	. . . . . . . . . . . . 13 |- (g = w -> ((g (_ h \/ h (_ g) <-> (w (_ h \/ h (_ w)))
57		sseq2 2079	. . . . . . . . . . . . . 14 |- (h = v -> (w (_ h <-> w (_ v))
58		sseq1 2078	. . . . . . . . . . . . . 14 |- (h = v -> (h (_ w <-> v (_ w))
59	57, 58	orbi12d 626	. . . . . . . . . . . . 13 |- (h = v -> ((w (_ h \/ h (_ w) <-> (w (_ v \/ v (_ w)))
60	56, 59	rcla42v 1876	. . . . . . . . . . . 12 |- ((w e. C /\ v e. C) -> (A.g e. C A.h e. C (g (_ h \/ h (_ g) -> (w (_ v \/ v (_ w)))
61		rnss 3337	. . . . . . . . . . . . . . . . . . 19 |- (w (_ v -> ran w (_ ran v)
62	61	sseld 2063	. . . . . . . . . . . . . . . . . 18 |- (w (_ v -> (y e. ran w -> y e. ran v))
63	62	anim1d 559	. . . . . . . . . . . . . . . . 17 |- (w (_ v -> ((y e. ran w /\ z e. ran v) -> (y e. ran v /\ z e. ran v)))
64	5	infxpidmlem5 7507	. . . . . . . . . . . . . . . . 17 |- ((C (_ H /\ v e. C) -> ((y e. ran v /\ z e. ran v) -> <.y, z>. e. dom U. C))
65	63, 64	syl9r 58	. . . . . . . . . . . . . . . 16 |- ((C (_ H /\ v e. C) -> (w (_ v -> ((y e. ran w /\ z e. ran v) -> <.y, z>. e. dom U. C)))
66	65	adantrl 394	. . . . . . . . . . . . . . 15 |- ((C (_ H /\ (w e. C /\ v e. C)) -> (w (_ v -> ((y e. ran w /\ z e. ran v) -> <.y, z>. e. dom U. C)))
67		rnss 3337	. . . . . . . . . . . . . . . . . . 19 |- (v (_ w -> ran v (_ ran w)
68	67	sseld 2063	. . . . . . . . . . . . . . . . . 18 |- (v (_ w -> (z e. ran v -> z e. ran w))
69	68	anim2d 560	. . . . . . . . . . . . . . . . 17 |- (v (_ w -> ((y e. ran w /\ z e. ran v) -> (y e. ran w /\ z e. ran w)))
70	5	infxpidmlem5 7507	. . . . . . . . . . . . . . . . 17 |- ((C (_ H /\ w e. C) -> ((y e. ran w /\ z e. ran w) -> <.y, z>. e. dom U. C))
71	69, 70	syl9r 58	. . . . . . . . . . . . . . . 16 |- ((C (_ H /\ w e. C) -> (v (_ w -> ((y e. ran w /\ z e. ran v) -> <.y, z>. e. dom U. C)))
72	71	adantrr 395	. . . . . . . . . . . . . . 15 |- ((C (_ H /\ (w e. C /\ v e. C)) -> (v (_ w -> ((y e. ran w /\ z e. ran v) -> <.y, z>. e. dom U. C)))
73	66, 72	jaod 424	. . . . . . . . . . . . . 14 |- ((C (_ H /\ (w e. C /\ v e. C)) -> ((w (_ v \/ v (_ w) -> ((y e. ran w /\ z e. ran v) -> <.y, z>. e. dom U. C)))
74	73	ex 373	. . . . . . . . . . . . 13 |- (C (_ H -> ((w e. C