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

Metamath Proof Explorer

Theorem alephsing

Description: The cofinality of a limit aleph is the same as the cofinality of its argument, so if ( alephA ) < A , then ( alephA ) is singular. Conversely, if ( alephA ) is regular (i.e. weakly inaccessible), then ( alephA ) = A , so A has to be rather large (see alephfp ). Proposition 11.13 of TakeutiZaring p. 103. (Contributed by Mario Carneiro, 9-Mar-2013)

Ref Expression
Assertion alephsing ( Lim 𝐴 → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 alephfnon ⊢ ℵ Fn On
2 fnfun ⊢ ( ℵ Fn On → Fun ℵ )
3 1 2 ax-mp ⊢ Fun ℵ
4 simpl ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → 𝐴 ∈ V )
5 resfunexg ⊢ ( ( Fun ℵ ∧ 𝐴 ∈ V ) → ( ℵ ↾ 𝐴 ) ∈ V )
6 3 4 5 sylancr ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ↾ 𝐴 ) ∈ V )
7 limelon ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → 𝐴 ∈ On )
8 onss ⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
9 7 8 syl ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → 𝐴 ⊆ On )
10 fnssres ⊢ ( ( ℵ Fn On ∧ 𝐴 ⊆ On ) → ( ℵ ↾ 𝐴 ) Fn 𝐴 )
11 1 9 10 sylancr ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ↾ 𝐴 ) Fn 𝐴 )
12 fvres ⊢ ( 𝑦 ∈ 𝐴 → ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) = ( ℵ ‘ 𝑦 ) )
13 12 adantl ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) → ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) = ( ℵ ‘ 𝑦 ) )
14 alephord2i ⊢ ( 𝐴 ∈ On → ( 𝑦 ∈ 𝐴 → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ) )
15 14 imp ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) )
16 13 15 eqeltrd ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) → ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) )
17 7 16 sylan ⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) )
18 17 ralrimiva ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ∀ 𝑦 ∈ 𝐴 ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) )
19 fnfvrnss ⊢ ( ( ( ℵ ↾ 𝐴 ) Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ) → ran ( ℵ ↾ 𝐴 ) ⊆ ( ℵ ‘ 𝐴 ) )
20 11 18 19 syl2anc ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ran ( ℵ ↾ 𝐴 ) ⊆ ( ℵ ‘ 𝐴 ) )
21 df-f ⊢ ( ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ↔ ( ( ℵ ↾ 𝐴 ) Fn 𝐴 ∧ ran ( ℵ ↾ 𝐴 ) ⊆ ( ℵ ‘ 𝐴 ) ) )
22 11 20 21 sylanbrc ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) )
23 alephsmo ⊢ Smo ℵ
24 1 fndmi ⊢ dom ℵ = On
25 7 24 eleqtrrdi ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → 𝐴 ∈ dom ℵ )
26 smores ⊢ ( ( Smo ℵ ∧ 𝐴 ∈ dom ℵ ) → Smo ( ℵ ↾ 𝐴 ) )
27 23 25 26 sylancr ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → Smo ( ℵ ↾ 𝐴 ) )
28 alephlim ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) = ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) )
29 28 eleq2d ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( 𝑥 ∈ ( ℵ ‘ 𝐴 ) ↔ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ) )
30 eliun ⊢ ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ ( ℵ ‘ 𝑦 ) )
31 alephon ⊢ ( ℵ ‘ 𝑦 ) ∈ On
32 31 onelssi ⊢ ( 𝑥 ∈ ( ℵ ‘ 𝑦 ) → 𝑥 ⊆ ( ℵ ‘ 𝑦 ) )
33 32 reximi ⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ ( ℵ ‘ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) )
34 30 33 sylbi ⊢ ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) )
35 29 34 biimtrdi ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( 𝑥 ∈ ( ℵ ‘ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) )
36 35 ralrimiv ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) )
37 feq1 ⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ↔ ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ) )
38 smoeq ⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( Smo 𝑓 ↔ Smo ( ℵ ↾ 𝐴 ) ) )
39 fveq1 ⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( 𝑓 ‘ 𝑦 ) = ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) )
40 39 12 sylan9eq ⊢ ( ( 𝑓 = ( ℵ ↾ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑦 ) = ( ℵ ‘ 𝑦 ) )
41 40 sseq2d ⊢ ( ( 𝑓 = ( ℵ ↾ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ↔ 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) )
42 41 rexbidva ⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) )
43 42 ralbidv ⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) )
44 37 38 43 3anbi123d ⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ↔ ( ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo ( ℵ ↾ 𝐴 ) ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) ) )
45 44 spcegv ⊢ ( ( ℵ ↾ 𝐴 ) ∈ V → ( ( ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo ( ℵ ↾ 𝐴 ) ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ) )
46 45 imp ⊢ ( ( ( ℵ ↾ 𝐴 ) ∈ V ∧ ( ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo ( ℵ ↾ 𝐴 ) ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) )
47 6 22 27 36 46 syl13anc ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) )
48 alephon ⊢ ( ℵ ‘ 𝐴 ) ∈ On
49 cfcof ⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ On ∧ 𝐴 ∈ On ) → ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) ) )
50 48 7 49 sylancr ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) ) )
51 47 50 mpd ⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) )
52 51 expcom ⊢ ( Lim 𝐴 → ( 𝐴 ∈ V → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) ) )
53 cf0 ⊢ ( cf ‘ ∅ ) = ∅
54 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( ℵ ‘ 𝐴 ) = ∅ )
55 54 fveq2d ⊢ ( ¬ 𝐴 ∈ V → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ ∅ ) )
56 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( cf ‘ 𝐴 ) = ∅ )
57 53 55 56 3eqtr4a ⊢ ( ¬ 𝐴 ∈ V → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) )
58 52 57 pm2.61d1 ⊢ ( Lim 𝐴 → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) )