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 = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))}
infxpidmlem6.2	⊢ B = ran ∪C

Assertion

Ref	Expression
infxpidmlem7	⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → ∪C:(B × 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 ⊢ (∀g ∈ C ((Fun g ∧ Fun ◡g) ∧ ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) ↔ (∀g ∈ C (Fun g ∧ Fun ◡g) ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)))
2		fun11uni 2707	. . . . . . 7 ⊢ (∀g ∈ C ((Fun g ∧ Fun ◡g) ∧ ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → (Fun ∪C ∧ Fun ◡∪C))
3	1, 2	sylbir 176	. . . . . 6 ⊢ ((∀g ∈ C (Fun g ∧ Fun ◡g) ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → (Fun ∪C ∧ Fun ◡∪C))
4		ssel 1502	. . . . . . . 8 ⊢ (C ⊆ H → (g ∈ C → g ∈ H))
5		infxpidmlem.1	. . . . . . . . . 10 ⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))}
6		visset 1350	. . . . . . . . . 10 ⊢ g ∈ V
7	5, 6	infxpidmlem2 4934	. . . . . . . . 9 ⊢ (g ∈ H ↔ (g = ∅ ∨ ∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(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)–1-1-onto→x → g:(x × x)–1-1→x)
17		df-f1 2435	. . . . . . . . . . . . . 14 ⊢ (g:(x × x)–1-1→x ↔ (g:(x × x)–→x ∧ Fun ◡g))
18		ffun 2754	. . . . . . . . . . . . . . 15 ⊢ (g:(x × x)–→x → Fun g)
19	18	anim1i 269	. . . . . . . . . . . . . 14 ⊢ ((g:(x × x)–→x ∧ Fun ◡g) → (Fun g ∧ Fun ◡g))
20	17, 19	sylbi 174	. . . . . . . . . . . . 13 ⊢ (g:(x × x)–1-1→x → (Fun g ∧ Fun ◡g))
21	16, 20	syl 12	. . . . . . . . . . . 12 ⊢ (g:(x × x)–1-1-onto→x → (Fun g ∧ Fun ◡g))
22	21	adantl 305	. . . . . . . . . . 11 ⊢ (((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → (Fun g ∧ Fun ◡g))
23	22	19.23aiv 952	. . . . . . . . . 10 ⊢ (∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → (Fun g ∧ Fun ◡g))
24	15, 23	jaoi 275	. . . . . . . . 9 ⊢ ((g = ∅ ∨ ∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x)) → (Fun g ∧ Fun ◡g))
25	7, 24	sylbi 174	. . . . . . . 8 ⊢ (g ∈ H → (Fun g ∧ Fun ◡g))
26	4, 25	syl6 23	. . . . . . 7 ⊢ (C ⊆ H → (g ∈ C → (Fun g ∧ Fun ◡g)))
27	26	r19.21aiv 1259	. . . . . 6 ⊢ (C ⊆ H → ∀g ∈ C (Fun g ∧ Fun ◡g))
28	3, 27	sylan 343	. . . . 5 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → (Fun ∪C ∧ Fun ◡∪C))
29		ssel2 1503	. . . . . . . . . . . . . 14 ⊢ ((C ⊆ H ∧ g ∈ C) → g ∈ H)
30	5	infxpidmlem4 4936	. . . . . . . . . . . . . 14 ⊢ (g ∈ H → dom g = (ran g × ran g))
31	29, 30	syl 12	. . . . . . . . . . . . 13 ⊢ ((C ⊆ H ∧ g ∈ C) → dom g = (ran g × ran g))
32		ra4e 1244	. . . . . . . . . . . . . . . . . 18 ⊢ ((g ∈ C ∧ y ∈ ran g) → ∃g ∈ C y ∈ ran g)
33		infxpidmlem6.2	. . . . . . . . . . . . . . . . . . 19 ⊢ B = ran ∪C
34	5, 33	infxpidmlem6 4938	. . . . . . . . . . . . . . . . . 18 ⊢ (y ∈ B ↔ ∃g ∈ C y ∈ ran g)
35	32, 34	sylibr 175	. . . . . . . . . . . . . . . . 17 ⊢ ((g ∈ C ∧ y ∈ ran g) → y ∈ B)
36	35	exp 291	. . . . . . . . . . . . . . . 16 ⊢ (g ∈ C → (y ∈ ran g → y ∈ B))
37	36	ssrdv 1509	. . . . . . . . . . . . . . 15 ⊢ (g ∈ C → ran g ⊆ B)
38		ssxp 2487	. . . . . . . . . . . . . . . 16 ⊢ ((ran g ⊆ B ∧ ran g ⊆ B) → (ran g × ran g) ⊆ (B × B))
39	38	anidms 332	. . . . . . . . . . . . . . 15 ⊢ (ran g ⊆ B → (ran g × ran g) ⊆ (B × B))
40	37, 39	syl 12	. . . . . . . . . . . . . 14 ⊢ (g ∈ C → (ran g × ran g) ⊆ (B × B))
41	40	adantl 305	. . . . . . . . . . . . 13 ⊢ ((C ⊆ H ∧ g ∈ C) → (ran g × ran g) ⊆ (B × B))
42	31, 41	eqsstrd 1534	. . . . . . . . . . . 12 ⊢ ((C ⊆ H ∧ g ∈ C) → dom g ⊆ (B × B))
43	42	sseld 1506	. . . . . . . . . . 11 ⊢ ((C ⊆ H ∧ g ∈ C) → (y ∈ dom g → y ∈ (B × B)))
44	43	exp 291	. . . . . . . . . 10 ⊢ (C ⊆ H → (g ∈ C → (y ∈ dom g → y ∈ (B × B))))
45	44	r19.23adv 1286	. . . . . . . . 9 ⊢ (C ⊆ H → (∃g ∈ C y ∈ dom g → y ∈ (B × B)))
46		dmuni 2538	. . . . . . . . . . 11 ⊢ dom ∪C = ∪g ∈ C dom g
47	46	eleq2i 1153	. . . . . . . . . 10 ⊢ (y ∈ dom ∪C ↔ y ∈ ∪g ∈ C dom g)
48		eliun 1998	. . . . . . . . . 10 ⊢ (y ∈ ∪g ∈ C dom g ↔ ∃g ∈ C y ∈ dom g)
49	47, 48	bitr 151	. . . . . . . . 9 ⊢ (y ∈ dom ∪C ↔ ∃g ∈ C y ∈ dom g)
50	45, 49	syl5ib 181	. . . . . . . 8 ⊢ (C ⊆ H → (y ∈ dom ∪C → y ∈ (B × B)))
51	50	ssrdv 1509	. . . . . . 7 ⊢ (C ⊆ H → dom ∪C ⊆ (B × B))
52	51	adantr 306	. . . . . 6 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → dom ∪C ⊆ (B × B))
53		relxp 2486	. . . . . . . 8 ⊢ Rel (B × B)
54	53	a1i 7	. . . . . . 7 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → Rel (B × 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 ⊢ (∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g) → ((w ∈ C ∧ v ∈ C) → (w ⊆ v ∨ v ⊆ w)))
62	61	com12 13	. . . . . . . . . . . 12 ⊢ ((w ∈ C ∧ v ∈ C) → (∀g ∈ C ∀h ∈ 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 ∈ ran w → y ∈ ran v))
65	64	anim1d 432	. . . . . . . . . . . . . . . . 17 ⊢ (w ⊆ v → ((y ∈ ran w ∧ z ∈ ran v) → (y ∈ ran v ∧ z ∈ ran v)))
66	5	infxpidmlem5 4937	. . . . . . . . . . . . . . . . 17 ⊢ ((C ⊆ H ∧ v ∈ C) → ((y ∈ ran v ∧ z ∈ ran v) → ⟨y, z⟩ ∈ dom ∪C))
67	65, 66	syl9r 56	. . . . . . . . . . . . . . . 16 ⊢ ((C ⊆ H ∧ v ∈ C) → (w ⊆ v → ((y ∈ ran w ∧ z ∈ ran v) → ⟨y, z⟩ ∈ dom ∪C)))
68	67	adantrl 311	. . . . . . . . . . . . . . 15 ⊢ ((C ⊆ H ∧ (w ∈ C ∧ v ∈ C)) → (w ⊆ v → ((y ∈ ran w ∧ z ∈ ran v) → ⟨y, z⟩ ∈ dom ∪C)))
69		rnss 2558	. . . . . . . . . . . . . . . . . . 19 ⊢ (v ⊆ w → ran v ⊆ ran w)
70	69	sseld 1506	. . . . . . . . . . . . . . . . . 18 ⊢ (v ⊆ w → (z ∈ ran v → z ∈ ran w))
71	70	anim2d 433	. . . . . . . . . . . . . . . . 17 ⊢ (v ⊆ w → ((y ∈ ran w ∧ z ∈ ran v) → (y ∈ ran w ∧ z ∈ ran w)))
72	5	infxpidmlem5 4937	. . . . . . . . . . . . . . . . 17 ⊢ ((C ⊆ H ∧ w ∈ C) → ((y ∈ ran w ∧ z ∈ ran w) → ⟨y, z⟩ ∈ dom ∪C))
73	71, 72	syl9r 56	. . . . . . . . . . . . . . . 16 ⊢ ((C ⊆ H ∧ w ∈ C) → (v ⊆ w → ((y ∈ ran w ∧ z ∈ ran v) → ⟨y, z⟩ ∈ dom ∪C)))
74	73	adantrr 312	. . . . . . . . . . . . . . 15 ⊢ ((C ⊆ H ∧ (w ∈ C ∧ v ∈ C)) → (v ⊆ w → ((y ∈ ran w ∧ z ∈ ran v) → ⟨y, z⟩ ∈ dom ∪C)))
75	68, 74	jaod 329	. . . . . . . . . . . . . 14 ⊢ ((C ⊆ H ∧ (w ∈ C ∧ v ∈ C)) → ((w ⊆ v ∨ v ⊆ w) → ((y ∈ ran w ∧ z ∈ ran v) → ⟨y, z⟩ ∈ dom ∪C)))
76	75	exp 291	. . . . . . . . . . . . 13 ⊢ (C ⊆ H → ((w ∈ C ∧ v ∈ C) → ((w ⊆ v ∨ v ⊆ w) → ((y ∈ ran w ∧ z ∈ ran v) → ⟨y, z⟩ ∈ dom ∪C))))
77	76	com3l 34	. . . . . . . . . . . 12 ⊢ ((w ∈ C ∧ v ∈ C) → ((w ⊆ v ∨ v ⊆ w) → (C ⊆ H → ((y ∈ ran w ∧ z ∈ ran v) → ⟨y, z⟩ ∈ dom ∪C))))
78	62, 77	syld 27	. . . . . . . . . . 11 ⊢ ((w ∈ C ∧ v ∈ C) → (∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g) → (C ⊆ H → ((y ∈ ran w ∧ z ∈ ran v) → ⟨y, z⟩ ∈ dom ∪C))))
79	78	com13 33	. . . . . . . . . 10 ⊢ (C ⊆ H → (∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g) → ((w ∈ C ∧ v ∈ C) → ((y ∈ ran w ∧ z ∈ ran v) → ⟨y, z⟩ ∈ dom ∪C))))
80	79	imp 277	. . . . . . . . 9 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → ((w ∈ C ∧ v ∈ C) → ((y ∈ ran w ∧ z ∈ ran v) → ⟨y, z⟩ ∈ dom ∪C)))
81	80	r19.23advv 1288	. . . . . . . 8 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → (∃w ∈ C ∃v ∈ C (y ∈ ran w ∧ z ∈ ran v) → ⟨y, z⟩ ∈ dom ∪C))
82	5, 33	infxpidmlem6 4938	. . . . . . . . . 10 ⊢ (y ∈ B ↔ ∃w ∈ C y ∈ ran w)
83	5, 33	infxpidmlem6 4938	. . . . . . . . . 10 ⊢ (z ∈ B ↔ ∃v ∈ C z ∈ ran v)
84	82, 83	anbi12i 369	. . . . . . . . 9 ⊢ ((y ∈ B ∧ z ∈ B) ↔ (∃w ∈ C y ∈ ran w ∧ ∃v ∈ C z ∈ ran v))
85		visset 1350	. . . . . . . . . 10 ⊢ z ∈ V
86	85	opelxp 2452	. . . . . . . . 9 ⊢ (⟨y, z⟩ ∈ (B × B) ↔ (y ∈ B ∧ z ∈ B))
87		reeanv 1316	. . . . . . . . 9 ⊢ (∃w ∈ C ∃v ∈ C (y ∈ ran w ∧ z ∈ ran v) ↔ (∃w ∈ C y ∈ ran w ∧ ∃v ∈ C z ∈ ran v))
88	84, 86, 87	3bitr4 158	. . . . . . . 8 ⊢ (⟨y, z⟩ ∈ (B × B) ↔ ∃w ∈ C ∃v ∈ C (y ∈ ran w ∧ z ∈ ran v))
89	81, 88	syl5ib 181	. . . . . . 7 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → (⟨y, z⟩ ∈ (B × B) → ⟨y, z⟩ ∈ dom ∪C))
90	54, 89	relssdv 2482	. . . . . 6 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → (B × B) ⊆ dom ∪C)
91	52, 90	eqssd 1518	. . . . 5 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → dom ∪C = (B × B))
92	28, 91	jca 236	. . . 4 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → ((Fun ∪C ∧ Fun ◡∪C) ∧ dom ∪C = (B × B)))
93		an23 371	. . . . 5 ⊢ (((Fun ∪C ∧ Fun ◡∪C) ∧ dom ∪C = (B × B)) ↔ ((Fun ∪C ∧ dom ∪C = (B × B)) ∧ Fun ◡∪C))
94		df-fn 2433	. . . . . 6 ⊢ (∪C Fn (B × B) ↔ (Fun ∪C ∧ dom ∪C = (B × B)))
95	94	anbi1i 368	. . . . 5 ⊢ ((∪C Fn (B × B) ∧ Fun ◡∪C) ↔ ((Fun ∪C ∧ dom ∪C = (B × B)) ∧ Fun ◡∪C))
96	93, 95	bitr4 154	. . . 4 ⊢ (((Fun ∪C ∧ Fun ◡∪C) ∧ dom ∪C = (B × B)) ↔ (∪C Fn (B × B) ∧ Fun ◡∪C))
97	92, 96	sylib 173	. . 3 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → (∪C Fn (B × B) ∧ Fun ◡∪C))
98	33	cleqcomi 1105	. . 3 ⊢ ran ∪C = B
99	97, 98	jctir 241	. 2 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → ((∪C Fn (B × B) ∧ Fun ◡∪C) ∧ ran ∪C = B))
100		f1o2 2804	. . 3 ⊢ (∪C:(B × B)–1-1-onto→B ↔ (∪C Fn (B × B) ∧ Fun ◡∪C ∧ ran ∪C = B))
101		df-3an 583	. . 3 ⊢ ((∪C Fn (B × B) ∧ Fun ◡∪C ∧ ran ∪C = B) ↔ ((∪C Fn (B × B) ∧ Fun ◡∪C) ∧ ran ∪C = B))
102	100, 101	bitr 151	. 2 ⊢ (∪C:(B × B)–1-1-onto→B ↔ ((∪C Fn (B × B) ∧ Fun ◡∪C) ∧ ran ∪C = B))
103	99, 102	sylibr 175	1 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → ∪C:(B × B)–1-1-onto→B)

Syntax hints:   → wi 2   ∨ wo 195   ∧ wa 196   ∧ w3a 581  ∃wex 678   = weq 797  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202   ⊆ wss 1487  ∅c0 1707  ⟨cop 1810  ∪cuni 1919  ∪ciun 1994   class class class wbr 2054  ωcom 2372   × cxp 2408  ^◡ccnv 2409  dom cdm 2410  ran crn 2411  Rel wrel 2415  Fun wfun 2416   Fn wfn 2417  –→wf 2418  –1-1→wf1 2419  –1-1-onto→wf1o 2421   ≼ cdom 3272

This theorem is referenced by:  infxpidmlem8 4940

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-iun 1996  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437

metamath.org