Theorem infxpidmlem8 4940

Description: Lemma for infxpidm 4945. The union of a collection of chains C in the collection of bijections H belongs to H. This property will be needed to apply Zorn's Lemma in infxpidmlem9 4941.

Hypotheses

Ref	Expression
infxpidmlem.1	⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))}
infxpidmlem6.2	⊢ B = ran ∪C
infxpidmlem8.3	⊢ C ∈ V

Assertion

Ref	Expression
infxpidmlem8	⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → ∪C ∈ H)

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 infxpidmlem8

Step	Hyp	Ref	Expression
1		ssel2 1503	. . . . . . . . . . 11 ⊢ ((C ⊆ H ∧ g ∈ C) → g ∈ H)
2		infxpidmlem.1	. . . . . . . . . . . . . . 15 ⊢ H = {f∣(f = ∅ ∨ ∃t((ω ≼ t ∧ t ⊆ A) ∧ f:(t × t)–1-1-onto→t))}
3		visset 1350	. . . . . . . . . . . . . . 15 ⊢ g ∈ V
4	2, 3	infxpidmlem2 4934	. . . . . . . . . . . . . 14 ⊢ (g ∈ H ↔ (g = ∅ ∨ ∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x)))
5	4	biimp 133	. . . . . . . . . . . . 13 ⊢ (g ∈ H → (g = ∅ ∨ ∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x)))
6	5	ord 202	. . . . . . . . . . . 12 ⊢ (g ∈ H → (¬ g = ∅ → ∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x)))
7		f1ofo 2806	. . . . . . . . . . . . . . . . . 18 ⊢ (g:(x × x)–1-1-onto→x → g:(x × x)–onto→x)
8		forn 2789	. . . . . . . . . . . . . . . . . 18 ⊢ (g:(x × x)–onto→x → ran g = x)
9	7, 8	syl 12	. . . . . . . . . . . . . . . . 17 ⊢ (g:(x × x)–1-1-onto→x → ran g = x)
10	9	cleqcomd 1106	. . . . . . . . . . . . . . . 16 ⊢ (g:(x × x)–1-1-onto→x → x = ran g)
11	10	anim1i 269	. . . . . . . . . . . . . . 15 ⊢ ((g:(x × x)–1-1-onto→x ∧ (ω ≼ x ∧ x ⊆ A)) → (x = ran g ∧ (ω ≼ x ∧ x ⊆ A)))
12	11	ancoms 334	. . . . . . . . . . . . . 14 ⊢ (((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → (x = ran g ∧ (ω ≼ x ∧ x ⊆ A)))
13	12	19.22i 723	. . . . . . . . . . . . 13 ⊢ (∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → ∃x(x = ran g ∧ (ω ≼ x ∧ x ⊆ A)))
14		rnexg 2569	. . . . . . . . . . . . . . 15 ⊢ (g ∈ V → ran g ∈ V)
15	3, 14	ax-mp 6	. . . . . . . . . . . . . 14 ⊢ ran g ∈ V
16		breq2 2066	. . . . . . . . . . . . . . 15 ⊢ (x = ran g → (ω ≼ x ↔ ω ≼ ran g))
17		sseq1 1521	. . . . . . . . . . . . . . 15 ⊢ (x = ran g → (x ⊆ A ↔ ran g ⊆ A))
18	16, 17	anbi12d 476	. . . . . . . . . . . . . 14 ⊢ (x = ran g → ((ω ≼ x ∧ x ⊆ A) ↔ (ω ≼ ran g ∧ ran g ⊆ A)))
19	15, 18	ceqsexv 1371	. . . . . . . . . . . . 13 ⊢ (∃x(x = ran g ∧ (ω ≼ x ∧ x ⊆ A)) ↔ (ω ≼ ran g ∧ ran g ⊆ A))
20	13, 19	sylib 173	. . . . . . . . . . . 12 ⊢ (∃x((ω ≼ x ∧ x ⊆ A) ∧ g:(x × x)–1-1-onto→x) → (ω ≼ ran g ∧ ran g ⊆ A))
21	6, 20	syl6 23	. . . . . . . . . . 11 ⊢ (g ∈ H → (¬ g = ∅ → (ω ≼ ran g ∧ ran g ⊆ A)))
22	1, 21	syl 12	. . . . . . . . . 10 ⊢ ((C ⊆ H ∧ g ∈ C) → (¬ g = ∅ → (ω ≼ ran g ∧ ran g ⊆ A)))
23		domtr 3320	. . . . . . . . . . . . . . 15 ⊢ ((ω ≼ ran g ∧ ran g ≼ B) → ω ≼ B)
24		ra4e 1244	. . . . . . . . . . . . . . . . . . 19 ⊢ ((g ∈ C ∧ y ∈ ran g) → ∃g ∈ C y ∈ ran g)
25		infxpidmlem6.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ B = ran ∪C
26	2, 25	infxpidmlem6 4938	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ B ↔ ∃g ∈ C y ∈ ran g)
27	24, 26	sylibr 175	. . . . . . . . . . . . . . . . . 18 ⊢ ((g ∈ C ∧ y ∈ ran g) → y ∈ B)
28	27	exp 291	. . . . . . . . . . . . . . . . 17 ⊢ (g ∈ C → (y ∈ ran g → y ∈ B))
29	28	ssrdv 1509	. . . . . . . . . . . . . . . 16 ⊢ (g ∈ C → ran g ⊆ B)
30		ssdomg 3311	. . . . . . . . . . . . . . . . 17 ⊢ (ran g ∈ V → (ran g ⊆ B → ran g ≼ B))
31	15, 30	ax-mp 6	. . . . . . . . . . . . . . . 16 ⊢ (ran g ⊆ B → ran g ≼ B)
32	29, 31	syl 12	. . . . . . . . . . . . . . 15 ⊢ (g ∈ C → ran g ≼ B)
33	23, 32	sylan2 346	. . . . . . . . . . . . . 14 ⊢ ((ω ≼ ran g ∧ g ∈ C) → ω ≼ B)
34	33	exp 291	. . . . . . . . . . . . 13 ⊢ (ω ≼ ran g → (g ∈ C → ω ≼ B))
35	34	com12 13	. . . . . . . . . . . 12 ⊢ (g ∈ C → (ω ≼ ran g → ω ≼ B))
36	35	adantl 305	. . . . . . . . . . 11 ⊢ ((C ⊆ H ∧ g ∈ C) → (ω ≼ ran g → ω ≼ B))
37	36	adantrd 308	. . . . . . . . . 10 ⊢ ((C ⊆ H ∧ g ∈ C) → ((ω ≼ ran g ∧ ran g ⊆ A) → ω ≼ B))
38	22, 37	syld 27	. . . . . . . . 9 ⊢ ((C ⊆ H ∧ g ∈ C) → (¬ g = ∅ → ω ≼ B))
39	38	exp 291	. . . . . . . 8 ⊢ (C ⊆ H → (g ∈ C → (¬ g = ∅ → ω ≼ B)))
40	39	r19.23adv 1286	. . . . . . 7 ⊢ (C ⊆ H → (∃g ∈ C ¬ g = ∅ → ω ≼ B))
41		uni0b 1939	. . . . . . . . . 10 ⊢ (∪C = ∅ ↔ C ⊆ {∅})
42		dfss3 1498	. . . . . . . . . 10 ⊢ (C ⊆ {∅} ↔ ∀g ∈ C g ∈ {∅})
43		elsn 1820	. . . . . . . . . . 11 ⊢ (g ∈ {∅} ↔ g = ∅)
44	43	biral 1223	. . . . . . . . . 10 ⊢ (∀g ∈ C g ∈ {∅} ↔ ∀g ∈ C g = ∅)
45	41, 42, 44	3bitr 155	. . . . . . . . 9 ⊢ (∪C = ∅ ↔ ∀g ∈ C g = ∅)
46	45	negbii 162	. . . . . . . 8 ⊢ (¬ ∪C = ∅ ↔ ¬ ∀g ∈ C g = ∅)
47		rexnal 1210	. . . . . . . 8 ⊢ (∃g ∈ C ¬ g = ∅ ↔ ¬ ∀g ∈ C g = ∅)
48	46, 47	bitr4 154	. . . . . . 7 ⊢ (¬ ∪C = ∅ ↔ ∃g ∈ C ¬ g = ∅)
49	40, 48	syl5ib 181	. . . . . 6 ⊢ (C ⊆ H → (¬ ∪C = ∅ → ω ≼ B))
50		pm3.27 260	. . . . . . . . . . . . . 14 ⊢ ((ω ≼ ran g ∧ ran g ⊆ A) → ran g ⊆ A)
51	22, 50	syl6 23	. . . . . . . . . . . . 13 ⊢ ((C ⊆ H ∧ g ∈ C) → (¬ g = ∅ → ran g ⊆ A))
52		rneq 2555	. . . . . . . . . . . . . . 15 ⊢ (g = ∅ → ran g = ran ∅)
53		rn0 2567	. . . . . . . . . . . . . . 15 ⊢ ran ∅ = ∅
54	52, 53	syl6eq 1140	. . . . . . . . . . . . . 14 ⊢ (g = ∅ → ran g = ∅)
55		0ss 1725	. . . . . . . . . . . . . . 15 ⊢ ∅ ⊆ A
56	55	a1i 7	. . . . . . . . . . . . . 14 ⊢ (g = ∅ → ∅ ⊆ A)
57	54, 56	eqsstrd 1534	. . . . . . . . . . . . 13 ⊢ (g = ∅ → ran g ⊆ A)
58	51, 57	pm2.61d2 111	. . . . . . . . . . . 12 ⊢ ((C ⊆ H ∧ g ∈ C) → ran g ⊆ A)
59	58	sseld 1506	. . . . . . . . . . 11 ⊢ ((C ⊆ H ∧ g ∈ C) → (y ∈ ran g → y ∈ A))
60	59	exp 291	. . . . . . . . . 10 ⊢ (C ⊆ H → (g ∈ C → (y ∈ ran g → y ∈ A)))
61	60	r19.23adv 1286	. . . . . . . . 9 ⊢ (C ⊆ H → (∃g ∈ C y ∈ ran g → y ∈ A))
62	61, 26	syl5ib 181	. . . . . . . 8 ⊢ (C ⊆ H → (y ∈ B → y ∈ A))
63	62	ssrdv 1509	. . . . . . 7 ⊢ (C ⊆ H → B ⊆ A)
64	63	a1d 14	. . . . . 6 ⊢ (C ⊆ H → (¬ ∪C = ∅ → B ⊆ A))
65	49, 64	jcad 455	. . . . 5 ⊢ (C ⊆ H → (¬ ∪C = ∅ → (ω ≼ B ∧ B ⊆ A)))
66	65	adantr 306	. . . 4 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → (¬ ∪C = ∅ → (ω ≼ B ∧ B ⊆ A)))
67	2, 25	infxpidmlem7 4939	. . . . 5 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → ∪C:(B × B)–1-1-onto→B)
68	67	a1d 14	. . . 4 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → (¬ ∪C = ∅ → ∪C:(B × B)–1-1-onto→B))
69	66, 68	jcad 455	. . 3 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → (¬ ∪C = ∅ → ((ω ≼ B ∧ B ⊆ A) ∧ ∪C:(B × B)–1-1-onto→B)))
70		infxpidmlem8.3	. . . . 5 ⊢ C ∈ V
71	70	uniex 1947	. . . 4 ⊢ ∪C ∈ V
72		rnexg 2569	. . . . . 6 ⊢ (∪C ∈ V → ran ∪C ∈ V)
73	71, 72	ax-mp 6	. . . . 5 ⊢ ran ∪C ∈ V
74	25, 73	eqeltr 1159	. . . 4 ⊢ B ∈ V
75	2, 71, 74	infxpidmlem3 4935	. . 3 ⊢ (((ω ≼ B ∧ B ⊆ A) ∧ ∪C:(B × B)–1-1-onto→B) → ∪C ∈ H)
76	69, 75	syl6 23	. 2 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → (¬ ∪C = ∅ → ∪C ∈ H))
77		orc 225	. . 3 ⊢ (∪C = ∅ → (∪C = ∅ ∨ ∃x((ω ≼ x ∧ x ⊆ A) ∧ ∪C:(x × x)–1-1-onto→x)))
78	2, 71	infxpidmlem2 4934	. . 3 ⊢ (∪C ∈ H ↔ (∪C = ∅ ∨ ∃x((ω ≼ x ∧ x ⊆ A) ∧ ∪C:(x × x)–1-1-onto→x)))
79	77, 78	sylibr 175	. 2 ⊢ (∪C = ∅ → ∪C ∈ H)
80	76, 79	pm2.61d2 111	1 ⊢ ((C ⊆ H ∧ ∀g ∈ C ∀h ∈ C (g ⊆ h ∨ h ⊆ g)) → ∪C ∈ H)

Syntax hints:  ¬ wn 1   → wi 2   ∨ wo 195   ∧ wa 196  ∃wex 678  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  Vcvv 1348   ⊆ wss 1487  ∅c0 1707  {csn 1808  ∪cuni 1919   class class class wbr 2054  ωcom 2372   × cxp 2408  ran crn 2411  –onto→wfo 2420  –1-1-onto→wf1o 2421   ≼ cdom 3272

This theorem is referenced by:  infxpidmlem9 4941

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-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-en 3274  df-dom 3275

metamath.org