Theorem infxpidmlem7 4939

Description: Lemma for infxpidm 4945. 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 group(s):   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 1289	. . . . . . 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 2707	. . . . . . 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 176	. . . . . 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 1502	. . . . . . . 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 1350	. . . . . . . . . 10 |- g e. V
7	5, 6	infxpidmlem2 4934	. . . . . . . . 9 |- (g e. H <-> (g = (/) \/ E.x((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x)))
8		f10 2822	. . . . . . . . . . . 12 |- (/):(/)-1-1->(/)
9		f1eq1 2776	. . . . . . . . . . . 12 |- (g = (/) -> (g:(/)-1-1->(/) <-> (/):(/)-1-1->(/)))
10	8, 9	mpbiri 169	. . . . . . . . . . 11 |- (g = (/) -> g:(/)-1-1->(/))
11		df-f1 2435	. . . . . . . . . . . 12 |- (g:(/)-1-1->(/) <-> (g:(/)-->(/) /\ Fun `'g))
12		ffun 2754	. . . . . . . . . . . . 13 |- (g:(/)-->(/) -> Fun g)
13	12	anim1i 269	. . . . . . . . . . . 12 |- ((g:(/)-->(/) /\ Fun `'g) -> (Fun g /\ Fun `'g))
14	11, 13	sylbi 174	. . . . . . . . . . 11 |- (g:(/)-1-1->(/) -> (Fun g /\ Fun `'g))
15	10, 14	syl 12	. . . . . . . . . 10 |- (g = (/) -> (Fun g /\ Fun `'g))
16		f1of1 2799	. . . . . . . . . . . . 13 |- (g:(x X. x)-1-1-onto->x -> g:(x X. x)-1-1->x)
17		df-f1 2435	. . . . . . . . . . . . . 14 |- (g:(x X. x)-1-1->x <-> (g:(x X. x)-->x /\ Fun `'g))
18		ffun 2754	. . . . . . . . . . . . . . 15 |- (g:(x X. x)-->x -> Fun g)
19	18	anim1i 269	. . . . . . . . . . . . . 14 |- ((g:(x X. x)-->x /\ Fun `'g) -> (Fun g /\ Fun `'g))
20	17, 19	sylbi 174	. . . . . . . . . . . . 13 |- (g:(x X. x)-1-1->x -> (Fun g /\ Fun `'g))
21	16, 20	syl 12	. . . . . . . . . . . 12 |- (g:(x X. x)-1-1-onto->x -> (Fun g /\ Fun `'g))
22	21	adantl 305	. . . . . . . . . . 11 |- (((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) -> (Fun g /\ Fun `'g))
23	22	19.23aiv 952	. . . . . . . . . 10 |- (E.x((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x) -> (Fun g /\ Fun `'g))
24	15, 23	jaoi 275	. . . . . . . . 9 |- ((g = (/) \/ E.x((om ~<_ x /\ x (_ A) /\ g:(x X. x)-1-1-onto->x)) -> (Fun g /\ Fun `'g))
25	7, 24	sylbi 174	. . . . . . . 8 |- (g e. H -> (Fun g /\ Fun `'g))
26	4, 25	syl6 23	. . . . . . 7 |- (C (_ H -> (g e. C -> (Fun g /\ Fun `'g)))
27	26	r19.21aiv 1259	. . . . . 6 |- (C (_ H -> A.g e. C (Fun g /\ Fun `'g))
28	3, 27	sylan 343	. . . . 5 |- ((C (_ H /\ A.g e. C A.h e. C (g (_ h \/ h (_ g)) -> (Fun U.C /\ Fun `'U.C))
29		ssel2 1503	. . . . . . . . . . . . . 14 |- ((C (_ H /\ g e. C) -> g e. H)
30	5	infxpidmlem4 4936	. . . . . . . . . . . . . 14 |- (g e. H -> dom g = (ran g X. ran g))
31	29, 30	syl 12	. . . . . . . . . . . . 13 |- ((C (_ H /\ g e. C) -> dom g = (ran g X. ran g))
32		ra4e 1244	. . . . . . . . . . . . . . . . . 18 |- ((g e. C /\ y e. ran g) -> E.g e. C y e. ran g)
33		infxpidmlem6.2	. . . . . . . . . . . . . . . . . . 19 |- B = ran U.C
34	5, 33	infxpidmlem6 4938	. . . . . . . . . . . . . . . . . 18 |- (y e. B <-> E.g e. C y e. ran g)
35	32, 34	sylibr 175	. . . . . . . . . . . . . . . . 17 |- ((g e. C /\ y e. ran g) -> y e. B)
36	35	exp 291	. . . . . . . . . . . . . . . 16 |- (g e. C -> (y e. ran g -> y e. B))
37	36	ssrdv 1509	. . . . . . . . . . . . . . 15 |- (g e. C -> ran g (_ B)
38		ssxp 2487	. . . . . . . . . . . . . . . 16 |- ((ran g (_ B /\ ran g (_ B) -> (ran g X. ran g) (_ (B X. B))
39	38	anidms 332	. . . . . . . . . . . . . . 15 |- (ran g (_ B -> (ran g X. ran g) (_ (B X. B))
40	37, 39	syl 12	. . . . . . . . . . . . . 14 |- (g e. C -> (ran g X. ran g) (_ (B X. B))
41	40	adantl 305	. . . . . . . . . . . . 13 |- ((C (_ H /\ g e. C) -> (ran g X. ran g) (_ (B X. B))
42	31, 41	eqsstrd 1534	. . . . . . . . . . . 12 |- ((C (_ H /\ g e. C) -> dom g (_ (B X. B))
43	42	sseld 1506	. . . . . . . . . . 11 |- ((C (_ H /\ g e. C) -> (y e. dom g -> y e. (B X. B)))
44	43	exp 291	. . . . . . . . . 10 |- (C (_ H -> (g e. C -> (y e. dom g -> y e. (B X. B))))
45	44	r19.23adv 1286	. . . . . . . . 9 |- (C (_ H -> (E.g e. C y e. dom g -> y e. (B X. B)))
46		dmuni 2538	. . . . . . . . . . 11 |- dom U.C = U.g e. C dom g
47	46	eleq2i 1153	. . . . . . . . . 10 |- (y e. dom U.C <-> y e. U.g e. C dom g)
48		eliun 1998	. . . . . . . . . 10 |- (y e. U.g e. C dom g <-> E.g e. C y e. dom g)
49	47, 48	bitr 151	. . . . . . . . 9 |- (y e. dom U.C <-> E.g e. C y e. dom g)
50	45, 49	syl5ib 181	. . . . . . . 8 |- (C (_ H -> (y e. dom U.C -> y e. (B X. B)))
51	50	ssrdv 1509	. . . . . . 7 |- (C (_ H -> dom U.C (_ (B X. B))
52	51	adantr 306	. . . . . 6 |- ((C (_ H /\ A.g e. C A.h e. C (g (_ h \/ h (_ g)) -> dom U.C (_ (B X. B))
53		relxp 2486	. . . . . . . 8 |- Rel (B X. B)
54	53	a1i 7	. . . . . . 7 |- ((C (_ H /\ A.g e. C A.h e. C (g (_ h \/ h (_ g)) -> Rel (B X. B))
55		sseq1 1521	. . . . . . . . . . . . . . 15 |- (g = w -> (g (_ h <-> w (_ h))
56		sseq2 1522	. . . . . . . . . . . . . . 15 |- (g = w -> (h (_ g <-> h (_ w))
57	55, 56	orbi12d 475	. . . . . . . . . . . . . 14 |- (g = w -> ((g (_ h \/ h (_ g) <-> (w (_ h \/ h (_ w)))
58		sseq2 1522	. . . . . . . . . . . . . . 15 |- (h = v -> (w (_ h <-> w (_ v))
59		sseq1 1521	. . . . . . . . . . . . . . 15 |- (h = v -> (h (_ w <-> v (_ w))
60	58, 59	orbi12d 475	. . . . . . . . . . . . . 14 |- (h = v -> ((w (_ h \/ h (_ w) <-> (w (_ v \/ v (_ w)))
61	57, 60	rcla42v 1404	. . . . . . . . . . . . 13 |- (A.g e. C A.h e. C (g (_ h \/ h (_ g) -> ((w e. C /\ v e. C) -> (w (_ v \/ v (_ w)))
62	61	com12 13	. . . . . . . . . . . 12 |- ((w e. C /\ v e. C) -> (A.g e. C A.h e. C (g (_ h \/ h (_ g) -> (w (_ v \/ v (_ w)))
63		rnss 2558	. . . . . . . . . . . . . . . . . . 19 |- (w (_ v -> ran w (_ ran v)
64	63	sseld 1506	. . . . . . . . . . . . . . . . . 18 |- (w (_ v -> (y e. ran w -> y e. ran v))
65	64	anim1d 432	. . . . . . . . . . . . . . . . 17 |- (w (_ v -> ((y e. ran w /\ z e. ran v) -> (y e. ran v /\ z e. ran v)))
66	5	infxpidmlem5 4937	. . . . . . . . . . . . . . . . 17 |- ((C (_ H /\ v e. C) -> ((y e. ran v /\ z e. ran v) -> <.y, z>. e. dom U.C))
67	65, 66	syl9r 56	. . . . . . . . . . . . . . . 16 |- ((C (_ H /\ v e. C) -> (w (_ v -> ((y e. ran w /\ z e. ran v) -> <.y, z>. e. dom U.C)))
68	67	adantrl 311	. . . . . . . . . . . . . . 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)))
69		rnss 2558	. . . . . . . . . . . . . . . . . . 19 |- (v (_ w -> ran v (_ ran w)
70	69	sseld 1506	. . . . . . . . . . . . . . . . . 18 |- (v (_ w -> (z e. ran v -> z e. ran w))
71	70	anim2d 433	. . . . . . . . . . . . . . . . 17 |- (v (_ w -> ((y e. ran w /\ z e. ran v) -> (y e. ran w /\ z e. ran w)))
72	5	infxpidmlem5 4937	. . . . . . . . . . . . . . . . 17 |- ((C (_ H /\ w e. C) -> ((y e. ran w /\ z e. ran w) -> <.y, z>. e. dom U.C))
73	71, 72	syl9r 56	. . . . . . . . . . . . . . . 16 |- ((C (_ H /\ w e. C) -> (v (_ w -> ((y e. ran w /\ z e. ran v) -> <.y, z>. e. dom U.C)))
74	73	adantrr 312	. . . . . . . . . . . . . . 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)))
75	68, 74	jaod 329	. . . . . . . . . . . . . 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)))
76	75	exp 291	. . . . . . . . . . . . 13 |- (C (_ H -> ((w e. C /\ v e. C) -> ((w (_ v \/ v <