This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdm ⊢ ( ( 𝑓 : ( 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 onsuc ⊢ ( 𝐴 ∈ 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 imbitrrid ⊢ ( 𝐴 ∈ 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 imbitrrid ⊢ ( 𝐴 ∈ 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 onsucb ⊢ ( 𝐴 ∈ 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 𝐴 )