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 biimtrdi 
 |-  ( ( 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 ) )