Metamath Proof Explorer

Theorem alephreg

Description: A successor aleph is regular. Theorem 11.15 of TakeutiZaring p. 103. (Contributed by Mario Carneiro, 9-Mar-2013)

Ref Expression
Assertion alephreg ⊢cf⁡ℵ⁡suc⁡A=ℵ⁡suc⁡A

Proof

Step Hyp Ref Expression
1 alephordilem1 ⊢A∈On→ℵ⁡A≺ℵ⁡suc⁡A
2 alephon ⊢ℵ⁡suc⁡A∈On
3 cff1 ⊢ℵ⁡suc⁡A∈On→∃ff:cf⁡ℵ⁡suc⁡A⟶1-1ℵ⁡suc⁡A∧∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y
4 2 3 ax-mp ⊢∃ff:cf⁡ℵ⁡suc⁡A⟶1-1ℵ⁡suc⁡A∧∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y
5 fvex ⊢cf⁡ℵ⁡suc⁡A∈V
6 fvex ⊢f⁡y∈V
7 6 sucex ⊢suc⁡f⁡y∈V
8 5 7 iunex ⊢⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y∈V
9 f1f ⊢f:cf⁡ℵ⁡suc⁡A⟶1-1ℵ⁡suc⁡A→f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A
10 9 ad2antrr ⊢f:cf⁡ℵ⁡suc⁡A⟶1-1ℵ⁡suc⁡A∧∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y∧A∈On∧cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A
11 simplr ⊢f:cf⁡ℵ⁡suc⁡A⟶1-1ℵ⁡suc⁡A∧∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y∧A∈On∧cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y
12 2 oneli ⊢x∈ℵ⁡suc⁡A→x∈On
13 ffvelcdm ⊢f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A∧y∈cf⁡ℵ⁡suc⁡A→f⁡y∈ℵ⁡suc⁡A
14 onelon ⊢ℵ⁡suc⁡A∈On∧f⁡y∈ℵ⁡suc⁡A→f⁡y∈On
15 2 13 14 sylancr ⊢f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A∧y∈cf⁡ℵ⁡suc⁡A→f⁡y∈On
16 onsssuc ⊢x∈On∧f⁡y∈On→x⊆f⁡y↔x∈suc⁡f⁡y
17 15 16 sylan2 ⊢x∈On∧f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A∧y∈cf⁡ℵ⁡suc⁡A→x⊆f⁡y↔x∈suc⁡f⁡y
18 17 anassrs ⊢x∈On∧f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A∧y∈cf⁡ℵ⁡suc⁡A→x⊆f⁡y↔x∈suc⁡f⁡y
19 18 rexbidva ⊢x∈On∧f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A→∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y↔∃y∈cf⁡ℵ⁡suc⁡Ax∈suc⁡f⁡y
20 eliun ⊢x∈⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y↔∃y∈cf⁡ℵ⁡suc⁡Ax∈suc⁡f⁡y
21 19 20 bitr4di ⊢x∈On∧f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A→∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y↔x∈⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y
22 21 ancoms ⊢f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A∧x∈On→∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y↔x∈⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y
23 12 22 sylan2 ⊢f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A∧x∈ℵ⁡suc⁡A→∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y↔x∈⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y
24 23 ralbidva ⊢f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A→∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y↔∀x∈ℵ⁡suc⁡Ax∈⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y
25 dfss3 ⊢ℵ⁡suc⁡A⊆⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y↔∀x∈ℵ⁡suc⁡Ax∈⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y
26 24 25 bitr4di ⊢f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A→∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y↔ℵ⁡suc⁡A⊆⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y
27 26 biimpa ⊢f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A∧∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y→ℵ⁡suc⁡A⊆⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y
28 10 11 27 syl2anc ⊢f:cf⁡ℵ⁡suc⁡A⟶1-1ℵ⁡suc⁡A∧∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y∧A∈On∧cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→ℵ⁡suc⁡A⊆⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y
29 ssdomg ⊢⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y∈V→ℵ⁡suc⁡A⊆⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y→ℵ⁡suc⁡A≼⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y
30 8 28 29 mpsyl ⊢f:cf⁡ℵ⁡suc⁡A⟶1-1ℵ⁡suc⁡A∧∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y∧A∈On∧cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→ℵ⁡suc⁡A≼⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y
31 simprl ⊢f:cf⁡ℵ⁡suc⁡A⟶1-1ℵ⁡suc⁡A∧∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y∧A∈On∧cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→A∈On
32 onsuc ⊢A∈On→suc⁡A∈On
33 alephislim ⊢suc⁡A∈On↔Lim⁡ℵ⁡suc⁡A
34 limsuc ⊢Lim⁡ℵ⁡suc⁡A→f⁡y∈ℵ⁡suc⁡A↔suc⁡f⁡y∈ℵ⁡suc⁡A
35 33 34 sylbi ⊢suc⁡A∈On→f⁡y∈ℵ⁡suc⁡A↔suc⁡f⁡y∈ℵ⁡suc⁡A
36 32 35 syl ⊢A∈On→f⁡y∈ℵ⁡suc⁡A↔suc⁡f⁡y∈ℵ⁡suc⁡A
37 breq1 ⊢z=suc⁡f⁡y→z≺ℵ⁡suc⁡A↔suc⁡f⁡y≺ℵ⁡suc⁡A
38 alephcard ⊢card⁡ℵ⁡suc⁡A=ℵ⁡suc⁡A
39 iscard ⊢card⁡ℵ⁡suc⁡A=ℵ⁡suc⁡A↔ℵ⁡suc⁡A∈On∧∀z∈ℵ⁡suc⁡Az≺ℵ⁡suc⁡A
40 39 simprbi ⊢card⁡ℵ⁡suc⁡A=ℵ⁡suc⁡A→∀z∈ℵ⁡suc⁡Az≺ℵ⁡suc⁡A
41 38 40 ax-mp ⊢∀z∈ℵ⁡suc⁡Az≺ℵ⁡suc⁡A
42 37 41 vtoclri ⊢suc⁡f⁡y∈ℵ⁡suc⁡A→suc⁡f⁡y≺ℵ⁡suc⁡A
43 alephsucdom ⊢A∈On→suc⁡f⁡y≼ℵ⁡A↔suc⁡f⁡y≺ℵ⁡suc⁡A
44 42 43 imbitrrid ⊢A∈On→suc⁡f⁡y∈ℵ⁡suc⁡A→suc⁡f⁡y≼ℵ⁡A
45 36 44 sylbid ⊢A∈On→f⁡y∈ℵ⁡suc⁡A→suc⁡f⁡y≼ℵ⁡A
46 13 45 syl5 ⊢A∈On→f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A∧y∈cf⁡ℵ⁡suc⁡A→suc⁡f⁡y≼ℵ⁡A
47 46 expdimp ⊢A∈On∧f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A→y∈cf⁡ℵ⁡suc⁡A→suc⁡f⁡y≼ℵ⁡A
48 47 ralrimiv ⊢A∈On∧f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A→∀y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y≼ℵ⁡A
49 iundom ⊢cf⁡ℵ⁡suc⁡A∈V∧∀y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y≼ℵ⁡A→⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y≼cf⁡ℵ⁡suc⁡A×ℵ⁡A
50 5 48 49 sylancr ⊢A∈On∧f:cf⁡ℵ⁡suc⁡A⟶ℵ⁡suc⁡A→⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y≼cf⁡ℵ⁡suc⁡A×ℵ⁡A
51 31 10 50 syl2anc ⊢f:cf⁡ℵ⁡suc⁡A⟶1-1ℵ⁡suc⁡A∧∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y∧A∈On∧cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y≼cf⁡ℵ⁡suc⁡A×ℵ⁡A
52 domtr ⊢ℵ⁡suc⁡A≼⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y∧⋃y∈cf⁡ℵ⁡suc⁡Asuc⁡f⁡y≼cf⁡ℵ⁡suc⁡A×ℵ⁡A→ℵ⁡suc⁡A≼cf⁡ℵ⁡suc⁡A×ℵ⁡A
53 30 51 52 syl2anc ⊢f:cf⁡ℵ⁡suc⁡A⟶1-1ℵ⁡suc⁡A∧∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y∧A∈On∧cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→ℵ⁡suc⁡A≼cf⁡ℵ⁡suc⁡A×ℵ⁡A
54 53 expcom ⊢A∈On∧cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→f:cf⁡ℵ⁡suc⁡A⟶1-1ℵ⁡suc⁡A∧∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y→ℵ⁡suc⁡A≼cf⁡ℵ⁡suc⁡A×ℵ⁡A
55 54 exlimdv ⊢A∈On∧cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→∃ff:cf⁡ℵ⁡suc⁡A⟶1-1ℵ⁡suc⁡A∧∀x∈ℵ⁡suc⁡A∃y∈cf⁡ℵ⁡suc⁡Ax⊆f⁡y→ℵ⁡suc⁡A≼cf⁡ℵ⁡suc⁡A×ℵ⁡A
56 4 55 mpi ⊢A∈On∧cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→ℵ⁡suc⁡A≼cf⁡ℵ⁡suc⁡A×ℵ⁡A
57 alephgeom ⊢A∈On↔ω⊆ℵ⁡A
58 alephon ⊢ℵ⁡A∈On
59 infxpen ⊢ℵ⁡A∈On∧ω⊆ℵ⁡A→ℵ⁡A×ℵ⁡A≈ℵ⁡A
60 58 59 mpan ⊢ω⊆ℵ⁡A→ℵ⁡A×ℵ⁡A≈ℵ⁡A
61 57 60 sylbi ⊢A∈On→ℵ⁡A×ℵ⁡A≈ℵ⁡A
62 breq1 ⊢z=cf⁡ℵ⁡suc⁡A→z≺ℵ⁡suc⁡A↔cf⁡ℵ⁡suc⁡A≺ℵ⁡suc⁡A
63 62 41 vtoclri ⊢cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→cf⁡ℵ⁡suc⁡A≺ℵ⁡suc⁡A
64 alephsucdom ⊢A∈On→cf⁡ℵ⁡suc⁡A≼ℵ⁡A↔cf⁡ℵ⁡suc⁡A≺ℵ⁡suc⁡A
65 63 64 imbitrrid ⊢A∈On→cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→cf⁡ℵ⁡suc⁡A≼ℵ⁡A
66 fvex ⊢ℵ⁡A∈V
67 66 xpdom1 ⊢cf⁡ℵ⁡suc⁡A≼ℵ⁡A→cf⁡ℵ⁡suc⁡A×ℵ⁡A≼ℵ⁡A×ℵ⁡A
68 65 67 syl6 ⊢A∈On→cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→cf⁡ℵ⁡suc⁡A×ℵ⁡A≼ℵ⁡A×ℵ⁡A
69 domentr ⊢cf⁡ℵ⁡suc⁡A×ℵ⁡A≼ℵ⁡A×ℵ⁡A∧ℵ⁡A×ℵ⁡A≈ℵ⁡A→cf⁡ℵ⁡suc⁡A×ℵ⁡A≼ℵ⁡A
70 69 expcom ⊢ℵ⁡A×ℵ⁡A≈ℵ⁡A→cf⁡ℵ⁡suc⁡A×ℵ⁡A≼ℵ⁡A×ℵ⁡A→cf⁡ℵ⁡suc⁡A×ℵ⁡A≼ℵ⁡A
71 61 68 70 sylsyld ⊢A∈On→cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→cf⁡ℵ⁡suc⁡A×ℵ⁡A≼ℵ⁡A
72 71 imp ⊢A∈On∧cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→cf⁡ℵ⁡suc⁡A×ℵ⁡A≼ℵ⁡A
73 domtr ⊢ℵ⁡suc⁡A≼cf⁡ℵ⁡suc⁡A×ℵ⁡A∧cf⁡ℵ⁡suc⁡A×ℵ⁡A≼ℵ⁡A→ℵ⁡suc⁡A≼ℵ⁡A
74 56 72 73 syl2anc ⊢A∈On∧cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→ℵ⁡suc⁡A≼ℵ⁡A
75 domnsym ⊢ℵ⁡suc⁡A≼ℵ⁡A→¬ℵ⁡A≺ℵ⁡suc⁡A
76 74 75 syl ⊢A∈On∧cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→¬ℵ⁡A≺ℵ⁡suc⁡A
77 76 ex ⊢A∈On→cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→¬ℵ⁡A≺ℵ⁡suc⁡A
78 1 77 mt2d ⊢A∈On→¬cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A
79 cfon ⊢cf⁡ℵ⁡suc⁡A∈On
80 cfle ⊢cf⁡ℵ⁡suc⁡A⊆ℵ⁡suc⁡A
81 onsseleq ⊢cf⁡ℵ⁡suc⁡A∈On∧ℵ⁡suc⁡A∈On→cf⁡ℵ⁡suc⁡A⊆ℵ⁡suc⁡A↔cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A∨cf⁡ℵ⁡suc⁡A=ℵ⁡suc⁡A
82 80 81 mpbii ⊢cf⁡ℵ⁡suc⁡A∈On∧ℵ⁡suc⁡A∈On→cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A∨cf⁡ℵ⁡suc⁡A=ℵ⁡suc⁡A
83 79 2 82 mp2an ⊢cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A∨cf⁡ℵ⁡suc⁡A=ℵ⁡suc⁡A
84 83 ori ⊢¬cf⁡ℵ⁡suc⁡A∈ℵ⁡suc⁡A→cf⁡ℵ⁡suc⁡A=ℵ⁡suc⁡A
85 78 84 syl ⊢A∈On→cf⁡ℵ⁡suc⁡A=ℵ⁡suc⁡A
86 cf0 ⊢cf⁡∅=∅
87 alephfnon ⊢ℵFnOn
88 87 fndmi ⊢dom⁡ℵ=On
89 88 eleq2i ⊢suc⁡A∈dom⁡ℵ↔suc⁡A∈On
90 onsucb ⊢A∈On↔suc⁡A∈On
91 89 90 bitr4i ⊢suc⁡A∈dom⁡ℵ↔A∈On
92 ndmfv ⊢¬suc⁡A∈dom⁡ℵ→ℵ⁡suc⁡A=∅
93 91 92 sylnbir ⊢¬A∈On→ℵ⁡suc⁡A=∅
94 93 fveq2d ⊢¬A∈On→cf⁡ℵ⁡suc⁡A=cf⁡∅
95 86 94 93 3eqtr4a ⊢¬A∈On→cf⁡ℵ⁡suc⁡A=ℵ⁡suc⁡A
96 85 95 pm2.61i ⊢cf⁡ℵ⁡suc⁡A=ℵ⁡suc⁡A