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 𝐴 ) ) = ( ℵ ‘ suc 𝐴 )

Proof

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