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 → ∃ f f : cf ⁡ ℵ ⁡ suc ⁡ A ⟶ 1-1 ℵ ⁡ suc ⁡ A ∧ ∀ x ∈ ℵ ⁡ suc ⁡ A ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ⊆ f ⁡ y
4 2 3 ax-mp ⊢ ∃ f f : cf ⁡ ℵ ⁡ suc ⁡ A ⟶ 1-1 ℵ ⁡ suc ⁡ A ∧ ∀ x ∈ ℵ ⁡ suc ⁡ A ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ⊆ 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 ⁡ A suc ⁡ 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 ⁡ A x ⊆ 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 ⁡ A x ⊆ f ⁡ y ∧ A ∈ On ∧ cf ⁡ ℵ ⁡ suc ⁡ A ∈ ℵ ⁡ suc ⁡ A → ∀ x ∈ ℵ ⁡ suc ⁡ A ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ⊆ f ⁡ y
12 2 oneli ⊢ x ∈ ℵ ⁡ suc ⁡ A → x ∈ On
13 ffvelrn ⊢ 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 ⁡ A x ⊆ f ⁡ y ↔ ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ∈ suc ⁡ f ⁡ y
20 eliun ⊢ x ∈ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y ↔ ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ∈ suc ⁡ f ⁡ y
21 19 20 syl6bbr ⊢ x ∈ On ∧ f : cf ⁡ ℵ ⁡ suc ⁡ A ⟶ ℵ ⁡ suc ⁡ A → ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ⊆ f ⁡ y ↔ x ∈ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y
22 21 ancoms ⊢ f : cf ⁡ ℵ ⁡ suc ⁡ A ⟶ ℵ ⁡ suc ⁡ A ∧ x ∈ On → ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ⊆ f ⁡ y ↔ x ∈ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y
23 12 22 sylan2 ⊢ f : cf ⁡ ℵ ⁡ suc ⁡ A ⟶ ℵ ⁡ suc ⁡ A ∧ x ∈ ℵ ⁡ suc ⁡ A → ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ⊆ f ⁡ y ↔ x ∈ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y
24 23 ralbidva ⊢ f : cf ⁡ ℵ ⁡ suc ⁡ A ⟶ ℵ ⁡ suc ⁡ A → ∀ x ∈ ℵ ⁡ suc ⁡ A ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ⊆ f ⁡ y ↔ ∀ x ∈ ℵ ⁡ suc ⁡ A x ∈ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y
25 dfss3 ⊢ ℵ ⁡ suc ⁡ A ⊆ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y ↔ ∀ x ∈ ℵ ⁡ suc ⁡ A x ∈ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y
26 24 25 syl6bbr ⊢ f : cf ⁡ ℵ ⁡ suc ⁡ A ⟶ ℵ ⁡ suc ⁡ A → ∀ x ∈ ℵ ⁡ suc ⁡ A ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ⊆ f ⁡ y ↔ ℵ ⁡ suc ⁡ A ⊆ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y
27 26 biimpa ⊢ f : cf ⁡ ℵ ⁡ suc ⁡ A ⟶ ℵ ⁡ suc ⁡ A ∧ ∀ x ∈ ℵ ⁡ suc ⁡ A ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ⊆ f ⁡ y → ℵ ⁡ suc ⁡ A ⊆ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y
28 10 11 27 syl2anc ⊢ f : cf ⁡ ℵ ⁡ suc ⁡ A ⟶ 1-1 ℵ ⁡ suc ⁡ A ∧ ∀ x ∈ ℵ ⁡ suc ⁡ A ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ⊆ f ⁡ y ∧ A ∈ On ∧ cf ⁡ ℵ ⁡ suc ⁡ A ∈ ℵ ⁡ suc ⁡ A → ℵ ⁡ suc ⁡ A ⊆ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y
29 ssdomg ⊢ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y ∈ V → ℵ ⁡ suc ⁡ A ⊆ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y → ℵ ⁡ suc ⁡ A ≼ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y
30 8 28 29 mpsyl ⊢ f : cf ⁡ ℵ ⁡ suc ⁡ A ⟶ 1-1 ℵ ⁡ suc ⁡ A ∧ ∀ x ∈ ℵ ⁡ suc ⁡ A ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ⊆ f ⁡ y ∧ A ∈ On ∧ cf ⁡ ℵ ⁡ suc ⁡ A ∈ ℵ ⁡ suc ⁡ A → ℵ ⁡ suc ⁡ A ≼ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y
31 simprl ⊢ f : cf ⁡ ℵ ⁡ suc ⁡ A ⟶ 1-1 ℵ ⁡ suc ⁡ A ∧ ∀ x ∈ ℵ ⁡ suc ⁡ A ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ⊆ f ⁡ y ∧ A ∈ On ∧ cf ⁡ ℵ ⁡ suc ⁡ A ∈ ℵ ⁡ suc ⁡ A → A ∈ On
32 suceloni ⊢ 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 ⁡ A z ≺ ℵ ⁡ suc ⁡ A
40 39 simprbi ⊢ card ⁡ ℵ ⁡ suc ⁡ A = ℵ ⁡ suc ⁡ A → ∀ z ∈ ℵ ⁡ suc ⁡ A z ≺ ℵ ⁡ suc ⁡ A
41 38 40 ax-mp ⊢ ∀ z ∈ ℵ ⁡ suc ⁡ A z ≺ ℵ ⁡ 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 syl5ibr ⊢ 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 ⁡ A suc ⁡ f ⁡ y ≼ ℵ ⁡ A
49 iundom ⊢ cf ⁡ ℵ ⁡ suc ⁡ A ∈ V ∧ ∀ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y ≼ ℵ ⁡ A → ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y ≼ cf ⁡ ℵ ⁡ suc ⁡ A × ℵ ⁡ A
50 5 48 49 sylancr ⊢ A ∈ On ∧ f : cf ⁡ ℵ ⁡ suc ⁡ A ⟶ ℵ ⁡ suc ⁡ A → ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ 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 ⁡ A x ⊆ f ⁡ y ∧ A ∈ On ∧ cf ⁡ ℵ ⁡ suc ⁡ A ∈ ℵ ⁡ suc ⁡ A → ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y ≼ cf ⁡ ℵ ⁡ suc ⁡ A × ℵ ⁡ A
52 domtr ⊢ ℵ ⁡ suc ⁡ A ≼ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ f ⁡ y ∧ ⋃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A suc ⁡ 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 ⁡ A x ⊆ 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 ⁡ A x ⊆ f ⁡ y → ℵ ⁡ suc ⁡ A ≼ cf ⁡ ℵ ⁡ suc ⁡ A × ℵ ⁡ A
55 54 exlimdv ⊢ A ∈ On ∧ cf ⁡ ℵ ⁡ suc ⁡ A ∈ ℵ ⁡ suc ⁡ A → ∃ f f : cf ⁡ ℵ ⁡ suc ⁡ A ⟶ 1-1 ℵ ⁡ suc ⁡ A ∧ ∀ x ∈ ℵ ⁡ suc ⁡ A ∃ y ∈ cf ⁡ ℵ ⁡ suc ⁡ A x ⊆ 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 syl5ibr ⊢ 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 ⊢ ℵ Fn On
88 fndm ⊢ ℵ Fn On → dom ⁡ ℵ = On
89 87 88 ax-mp ⊢ dom ⁡ ℵ = On
90 89 eleq2i ⊢ suc ⁡ A ∈ dom ⁡ ℵ ↔ suc ⁡ A ∈ On
91 sucelon ⊢ A ∈ On ↔ suc ⁡ A ∈ On
92 90 91 bitr4i ⊢ suc ⁡ A ∈ dom ⁡ ℵ ↔ A ∈ On
93 ndmfv ⊢ ¬ suc ⁡ A ∈ dom ⁡ ℵ → ℵ ⁡ suc ⁡ A = ∅
94 92 93 sylnbir ⊢ ¬ A ∈ On → ℵ ⁡ suc ⁡ A = ∅
95 94 fveq2d ⊢ ¬ A ∈ On → cf ⁡ ℵ ⁡ suc ⁡ A = cf ⁡ ∅
96 86 95 94 3eqtr4a ⊢ ¬ A ∈ On → cf ⁡ ℵ ⁡ suc ⁡ A = ℵ ⁡ suc ⁡ A
97 85 96 pm2.61i ⊢ cf ⁡ ℵ ⁡ suc ⁡ A = ℵ ⁡ suc ⁡ A