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 syl6bi ( ( 𝐴 ∈ 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 ‘ 𝐴 ) )