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 A -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) )

Proof

Step Hyp Ref Expression
1 alephfnon
 |-  aleph Fn On
2 fnfun
 |-  ( aleph Fn On -> Fun aleph )
3 1 2 ax-mp
 |-  Fun aleph
4 simpl
 |-  ( ( A e. _V /\ Lim A ) -> A e. _V )
5 resfunexg
 |-  ( ( Fun aleph /\ A e. _V ) -> ( aleph |` A ) e. _V )
6 3 4 5 sylancr
 |-  ( ( A e. _V /\ Lim A ) -> ( aleph |` A ) e. _V )
7 limelon
 |-  ( ( A e. _V /\ Lim A ) -> A e. On )
8 onss
 |-  ( A e. On -> A C_ On )
9 7 8 syl
 |-  ( ( A e. _V /\ Lim A ) -> A C_ On )
10 fnssres
 |-  ( ( aleph Fn On /\ A C_ On ) -> ( aleph |` A ) Fn A )
11 1 9 10 sylancr
 |-  ( ( A e. _V /\ Lim A ) -> ( aleph |` A ) Fn A )
12 fvres
 |-  ( y e. A -> ( ( aleph |` A ) ` y ) = ( aleph ` y ) )
13 12 adantl
 |-  ( ( A e. On /\ y e. A ) -> ( ( aleph |` A ) ` y ) = ( aleph ` y ) )
14 alephord2i
 |-  ( A e. On -> ( y e. A -> ( aleph ` y ) e. ( aleph ` A ) ) )
15 14 imp
 |-  ( ( A e. On /\ y e. A ) -> ( aleph ` y ) e. ( aleph ` A ) )
16 13 15 eqeltrd
 |-  ( ( A e. On /\ y e. A ) -> ( ( aleph |` A ) ` y ) e. ( aleph ` A ) )
17 7 16 sylan
 |-  ( ( ( A e. _V /\ Lim A ) /\ y e. A ) -> ( ( aleph |` A ) ` y ) e. ( aleph ` A ) )
18 17 ralrimiva
 |-  ( ( A e. _V /\ Lim A ) -> A. y e. A ( ( aleph |` A ) ` y ) e. ( aleph ` A ) )
19 fnfvrnss
 |-  ( ( ( aleph |` A ) Fn A /\ A. y e. A ( ( aleph |` A ) ` y ) e. ( aleph ` A ) ) -> ran ( aleph |` A ) C_ ( aleph ` A ) )
20 11 18 19 syl2anc
 |-  ( ( A e. _V /\ Lim A ) -> ran ( aleph |` A ) C_ ( aleph ` A ) )
21 df-f
 |-  ( ( aleph |` A ) : A --> ( aleph ` A ) <-> ( ( aleph |` A ) Fn A /\ ran ( aleph |` A ) C_ ( aleph ` A ) ) )
22 11 20 21 sylanbrc
 |-  ( ( A e. _V /\ Lim A ) -> ( aleph |` A ) : A --> ( aleph ` A ) )
23 alephsmo
 |-  Smo aleph
24 1 fndmi
 |-  dom aleph = On
25 7 24 eleqtrrdi
 |-  ( ( A e. _V /\ Lim A ) -> A e. dom aleph )
26 smores
 |-  ( ( Smo aleph /\ A e. dom aleph ) -> Smo ( aleph |` A ) )
27 23 25 26 sylancr
 |-  ( ( A e. _V /\ Lim A ) -> Smo ( aleph |` A ) )
28 alephlim
 |-  ( ( A e. _V /\ Lim A ) -> ( aleph ` A ) = U_ y e. A ( aleph ` y ) )
29 28 eleq2d
 |-  ( ( A e. _V /\ Lim A ) -> ( x e. ( aleph ` A ) <-> x e. U_ y e. A ( aleph ` y ) ) )
30 eliun
 |-  ( x e. U_ y e. A ( aleph ` y ) <-> E. y e. A x e. ( aleph ` y ) )
31 alephon
 |-  ( aleph ` y ) e. On
32 31 onelssi
 |-  ( x e. ( aleph ` y ) -> x C_ ( aleph ` y ) )
33 32 reximi
 |-  ( E. y e. A x e. ( aleph ` y ) -> E. y e. A x C_ ( aleph ` y ) )
34 30 33 sylbi
 |-  ( x e. U_ y e. A ( aleph ` y ) -> E. y e. A x C_ ( aleph ` y ) )
35 29 34 syl6bi
 |-  ( ( A e. _V /\ Lim A ) -> ( x e. ( aleph ` A ) -> E. y e. A x C_ ( aleph ` y ) ) )
36 35 ralrimiv
 |-  ( ( A e. _V /\ Lim A ) -> A. x e. ( aleph ` A ) E. y e. A x C_ ( aleph ` y ) )
37 feq1
 |-  ( f = ( aleph |` A ) -> ( f : A --> ( aleph ` A ) <-> ( aleph |` A ) : A --> ( aleph ` A ) ) )
38 smoeq
 |-  ( f = ( aleph |` A ) -> ( Smo f <-> Smo ( aleph |` A ) ) )
39 fveq1
 |-  ( f = ( aleph |` A ) -> ( f ` y ) = ( ( aleph |` A ) ` y ) )
40 39 12 sylan9eq
 |-  ( ( f = ( aleph |` A ) /\ y e. A ) -> ( f ` y ) = ( aleph ` y ) )
41 40 sseq2d
 |-  ( ( f = ( aleph |` A ) /\ y e. A ) -> ( x C_ ( f ` y ) <-> x C_ ( aleph ` y ) ) )
42 41 rexbidva
 |-  ( f = ( aleph |` A ) -> ( E. y e. A x C_ ( f ` y ) <-> E. y e. A x C_ ( aleph ` y ) ) )
43 42 ralbidv
 |-  ( f = ( aleph |` A ) -> ( A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) <-> A. x e. ( aleph ` A ) E. y e. A x C_ ( aleph ` y ) ) )
44 37 38 43 3anbi123d
 |-  ( f = ( aleph |` A ) -> ( ( f : A --> ( aleph ` A ) /\ Smo f /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) ) <-> ( ( aleph |` A ) : A --> ( aleph ` A ) /\ Smo ( aleph |` A ) /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( aleph ` y ) ) ) )
45 44 spcegv
 |-  ( ( aleph |` A ) e. _V -> ( ( ( aleph |` A ) : A --> ( aleph ` A ) /\ Smo ( aleph |` A ) /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( aleph ` y ) ) -> E. f ( f : A --> ( aleph ` A ) /\ Smo f /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) ) ) )
46 45 imp
 |-  ( ( ( aleph |` A ) e. _V /\ ( ( aleph |` A ) : A --> ( aleph ` A ) /\ Smo ( aleph |` A ) /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( aleph ` y ) ) ) -> E. f ( f : A --> ( aleph ` A ) /\ Smo f /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) ) )
47 6 22 27 36 46 syl13anc
 |-  ( ( A e. _V /\ Lim A ) -> E. f ( f : A --> ( aleph ` A ) /\ Smo f /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) ) )
48 alephon
 |-  ( aleph ` A ) e. On
49 cfcof
 |-  ( ( ( aleph ` A ) e. On /\ A e. On ) -> ( E. f ( f : A --> ( aleph ` A ) /\ Smo f /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) ) -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) ) )
50 48 7 49 sylancr
 |-  ( ( A e. _V /\ Lim A ) -> ( E. f ( f : A --> ( aleph ` A ) /\ Smo f /\ A. x e. ( aleph ` A ) E. y e. A x C_ ( f ` y ) ) -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) ) )
51 47 50 mpd
 |-  ( ( A e. _V /\ Lim A ) -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) )
52 51 expcom
 |-  ( Lim A -> ( A e. _V -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) ) )
53 cf0
 |-  ( cf ` (/) ) = (/)
54 fvprc
 |-  ( -. A e. _V -> ( aleph ` A ) = (/) )
55 54 fveq2d
 |-  ( -. A e. _V -> ( cf ` ( aleph ` A ) ) = ( cf ` (/) ) )
56 fvprc
 |-  ( -. A e. _V -> ( cf ` A ) = (/) )
57 53 55 56 3eqtr4a
 |-  ( -. A e. _V -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) )
58 52 57 pm2.61d1
 |-  ( Lim A -> ( cf ` ( aleph ` A ) ) = ( cf ` A ) )