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

Proof

Step Hyp Ref Expression
1 alephordilem1 
 |-  ( A e. On -> ( aleph ` A ) ~< ( aleph ` suc A ) )
2 alephon 
 |-  ( aleph ` suc A ) e. On
3 cff1 
 |-  ( ( aleph ` suc A ) e. On -> E. f ( f : ( cf ` ( aleph ` suc A ) ) -1-1-> ( aleph ` suc A ) /\ A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) ) )
4 2 3 ax-mp 
 |-  E. f ( f : ( cf ` ( aleph ` suc A ) ) -1-1-> ( aleph ` suc A ) /\ A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) )
5 fvex 
 |-  ( cf ` ( aleph ` suc A ) ) e. _V
6 fvex 
 |-  ( f ` y ) e. _V
7 6 sucex 
 |-  suc ( f ` y ) e. _V
8 5 7 iunex 
 |-  U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) e. _V
9 f1f 
 |-  ( f : ( cf ` ( aleph ` suc A ) ) -1-1-> ( aleph ` suc A ) -> f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) )
10 9 ad2antrr 
 |-  ( ( ( f : ( cf ` ( aleph ` suc A ) ) -1-1-> ( aleph ` suc A ) /\ A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) ) /\ ( A e. On /\ ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) ) ) -> f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) )
11 simplr 
 |-  ( ( ( f : ( cf ` ( aleph ` suc A ) ) -1-1-> ( aleph ` suc A ) /\ A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) ) /\ ( A e. On /\ ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) ) ) -> A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) )
12 2 oneli 
 |-  ( x e. ( aleph ` suc A ) -> x e. On )
13 ffvelcdm 
 |-  ( ( f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) /\ y e. ( cf ` ( aleph ` suc A ) ) ) -> ( f ` y ) e. ( aleph ` suc A ) )
14 onelon 
 |-  ( ( ( aleph ` suc A ) e. On /\ ( f ` y ) e. ( aleph ` suc A ) ) -> ( f ` y ) e. On )
15 2 13 14 sylancr 
 |-  ( ( f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) /\ y e. ( cf ` ( aleph ` suc A ) ) ) -> ( f ` y ) e. On )
16 onsssuc 
 |-  ( ( x e. On /\ ( f ` y ) e. On ) -> ( x C_ ( f ` y ) <-> x e. suc ( f ` y ) ) )
17 15 16 sylan2 
 |-  ( ( x e. On /\ ( f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) /\ y e. ( cf ` ( aleph ` suc A ) ) ) ) -> ( x C_ ( f ` y ) <-> x e. suc ( f ` y ) ) )
18 17 anassrs 
 |-  ( ( ( x e. On /\ f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) ) /\ y e. ( cf ` ( aleph ` suc A ) ) ) -> ( x C_ ( f ` y ) <-> x e. suc ( f ` y ) ) )
19 18 rexbidva 
 |-  ( ( x e. On /\ f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) ) -> ( E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) <-> E. y e. ( cf ` ( aleph ` suc A ) ) x e. suc ( f ` y ) ) )
20 eliun 
 |-  ( x e. U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) <-> E. y e. ( cf ` ( aleph ` suc A ) ) x e. suc ( f ` y ) )
21 19 20 bitr4di 
 |-  ( ( x e. On /\ f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) ) -> ( E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) <-> x e. U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) ) )
22 21 ancoms 
 |-  ( ( f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) /\ x e. On ) -> ( E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) <-> x e. U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) ) )
23 12 22 sylan2 
 |-  ( ( f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) /\ x e. ( aleph ` suc A ) ) -> ( E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) <-> x e. U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) ) )
24 23 ralbidva 
 |-  ( f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) -> ( A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) <-> A. x e. ( aleph ` suc A ) x e. U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) ) )
25 dfss3 
 |-  ( ( aleph ` suc A ) C_ U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) <-> A. x e. ( aleph ` suc A ) x e. U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) )
26 24 25 bitr4di 
 |-  ( f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) -> ( A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) <-> ( aleph ` suc A ) C_ U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) ) )
27 26 biimpa 
 |-  ( ( f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) /\ A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) ) -> ( aleph ` suc A ) C_ U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) )
28 10 11 27 syl2anc 
 |-  ( ( ( f : ( cf ` ( aleph ` suc A ) ) -1-1-> ( aleph ` suc A ) /\ A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) ) /\ ( A e. On /\ ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) ) ) -> ( aleph ` suc A ) C_ U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) )
29 ssdomg 
 |-  ( U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) e. _V -> ( ( aleph ` suc A ) C_ U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) -> ( aleph ` suc A ) ~<_ U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) ) )
30 8 28 29 mpsyl 
 |-  ( ( ( f : ( cf ` ( aleph ` suc A ) ) -1-1-> ( aleph ` suc A ) /\ A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) ) /\ ( A e. On /\ ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) ) ) -> ( aleph ` suc A ) ~<_ U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) )
31 simprl 
 |-  ( ( ( f : ( cf ` ( aleph ` suc A ) ) -1-1-> ( aleph ` suc A ) /\ A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) ) /\ ( A e. On /\ ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) ) ) -> A e. On )
32 onsuc 
 |-  ( A e. On -> suc A e. On )
33 alephislim 
 |-  ( suc A e. On <-> Lim ( aleph ` suc A ) )
34 limsuc 
 |-  ( Lim ( aleph ` suc A ) -> ( ( f ` y ) e. ( aleph ` suc A ) <-> suc ( f ` y ) e. ( aleph ` suc A ) ) )
35 33 34 sylbi 
 |-  ( suc A e. On -> ( ( f ` y ) e. ( aleph ` suc A ) <-> suc ( f ` y ) e. ( aleph ` suc A ) ) )
36 32 35 syl 
 |-  ( A e. On -> ( ( f ` y ) e. ( aleph ` suc A ) <-> suc ( f ` y ) e. ( aleph ` suc A ) ) )
37 breq1 
 |-  ( z = suc ( f ` y ) -> ( z ~< ( aleph ` suc A ) <-> suc ( f ` y ) ~< ( aleph ` suc A ) ) )
38 alephcard 
 |-  ( card ` ( aleph ` suc A ) ) = ( aleph ` suc A )
39 iscard 
 |-  ( ( card ` ( aleph ` suc A ) ) = ( aleph ` suc A ) <-> ( ( aleph ` suc A ) e. On /\ A. z e. ( aleph ` suc A ) z ~< ( aleph ` suc A ) ) )
40 39 simprbi 
 |-  ( ( card ` ( aleph ` suc A ) ) = ( aleph ` suc A ) -> A. z e. ( aleph ` suc A ) z ~< ( aleph ` suc A ) )
41 38 40 ax-mp 
 |-  A. z e. ( aleph ` suc A ) z ~< ( aleph ` suc A )
42 37 41 vtoclri 
 |-  ( suc ( f ` y ) e. ( aleph ` suc A ) -> suc ( f ` y ) ~< ( aleph ` suc A ) )
43 alephsucdom 
 |-  ( A e. On -> ( suc ( f ` y ) ~<_ ( aleph ` A ) <-> suc ( f ` y ) ~< ( aleph ` suc A ) ) )
44 42 43 imbitrrid 
 |-  ( A e. On -> ( suc ( f ` y ) e. ( aleph ` suc A ) -> suc ( f ` y ) ~<_ ( aleph ` A ) ) )
45 36 44 sylbid 
 |-  ( A e. On -> ( ( f ` y ) e. ( aleph ` suc A ) -> suc ( f ` y ) ~<_ ( aleph ` A ) ) )
46 13 45 syl5 
 |-  ( A e. On -> ( ( f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) /\ y e. ( cf ` ( aleph ` suc A ) ) ) -> suc ( f ` y ) ~<_ ( aleph ` A ) ) )
47 46 expdimp 
 |-  ( ( A e. On /\ f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) ) -> ( y e. ( cf ` ( aleph ` suc A ) ) -> suc ( f ` y ) ~<_ ( aleph ` A ) ) )
48 47 ralrimiv 
 |-  ( ( A e. On /\ f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) ) -> A. y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) ~<_ ( aleph ` A ) )
49 iundom 
 |-  ( ( ( cf ` ( aleph ` suc A ) ) e. _V /\ A. y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) ~<_ ( aleph ` A ) ) -> U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) ~<_ ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) )
50 5 48 49 sylancr 
 |-  ( ( A e. On /\ f : ( cf ` ( aleph ` suc A ) ) --> ( aleph ` suc A ) ) -> U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) ~<_ ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) )
51 31 10 50 syl2anc 
 |-  ( ( ( f : ( cf ` ( aleph ` suc A ) ) -1-1-> ( aleph ` suc A ) /\ A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) ) /\ ( A e. On /\ ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) ) ) -> U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) ~<_ ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) )
52 domtr 
 |-  ( ( ( aleph ` suc A ) ~<_ U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) /\ U_ y e. ( cf ` ( aleph ` suc A ) ) suc ( f ` y ) ~<_ ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) ) -> ( aleph ` suc A ) ~<_ ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) )
53 30 51 52 syl2anc 
 |-  ( ( ( f : ( cf ` ( aleph ` suc A ) ) -1-1-> ( aleph ` suc A ) /\ A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) ) /\ ( A e. On /\ ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) ) ) -> ( aleph ` suc A ) ~<_ ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) )
54 53 expcom 
 |-  ( ( A e. On /\ ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) ) -> ( ( f : ( cf ` ( aleph ` suc A ) ) -1-1-> ( aleph ` suc A ) /\ A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) ) -> ( aleph ` suc A ) ~<_ ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) ) )
55 54 exlimdv 
 |-  ( ( A e. On /\ ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) ) -> ( E. f ( f : ( cf ` ( aleph ` suc A ) ) -1-1-> ( aleph ` suc A ) /\ A. x e. ( aleph ` suc A ) E. y e. ( cf ` ( aleph ` suc A ) ) x C_ ( f ` y ) ) -> ( aleph ` suc A ) ~<_ ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) ) )
56 4 55 mpi 
 |-  ( ( A e. On /\ ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) ) -> ( aleph ` suc A ) ~<_ ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) )
57 alephgeom 
 |-  ( A e. On <-> _om C_ ( aleph ` A ) )
58 alephon 
 |-  ( aleph ` A ) e. On
59 infxpen 
 |-  ( ( ( aleph ` A ) e. On /\ _om C_ ( aleph ` A ) ) -> ( ( aleph ` A ) X. ( aleph ` A ) ) ~~ ( aleph ` A ) )
60 58 59 mpan 
 |-  ( _om C_ ( aleph ` A ) -> ( ( aleph ` A ) X. ( aleph ` A ) ) ~~ ( aleph ` A ) )
61 57 60 sylbi 
 |-  ( A e. On -> ( ( aleph ` A ) X. ( aleph ` A ) ) ~~ ( aleph ` A ) )
62 breq1 
 |-  ( z = ( cf ` ( aleph ` suc A ) ) -> ( z ~< ( aleph ` suc A ) <-> ( cf ` ( aleph ` suc A ) ) ~< ( aleph ` suc A ) ) )
63 62 41 vtoclri 
 |-  ( ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) -> ( cf ` ( aleph ` suc A ) ) ~< ( aleph ` suc A ) )
64 alephsucdom 
 |-  ( A e. On -> ( ( cf ` ( aleph ` suc A ) ) ~<_ ( aleph ` A ) <-> ( cf ` ( aleph ` suc A ) ) ~< ( aleph ` suc A ) ) )
65 63 64 imbitrrid 
 |-  ( A e. On -> ( ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) -> ( cf ` ( aleph ` suc A ) ) ~<_ ( aleph ` A ) ) )
66 fvex 
 |-  ( aleph ` A ) e. _V
67 66 xpdom1 
 |-  ( ( cf ` ( aleph ` suc A ) ) ~<_ ( aleph ` A ) -> ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) ~<_ ( ( aleph ` A ) X. ( aleph ` A ) ) )
68 65 67 syl6 
 |-  ( A e. On -> ( ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) -> ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) ~<_ ( ( aleph ` A ) X. ( aleph ` A ) ) ) )
69 domentr 
 |-  ( ( ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) ~<_ ( ( aleph ` A ) X. ( aleph ` A ) ) /\ ( ( aleph ` A ) X. ( aleph ` A ) ) ~~ ( aleph ` A ) ) -> ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) ~<_ ( aleph ` A ) )
70 69 expcom 
 |-  ( ( ( aleph ` A ) X. ( aleph ` A ) ) ~~ ( aleph ` A ) -> ( ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) ~<_ ( ( aleph ` A ) X. ( aleph ` A ) ) -> ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) ~<_ ( aleph ` A ) ) )
71 61 68 70 sylsyld 
 |-  ( A e. On -> ( ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) -> ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) ~<_ ( aleph ` A ) ) )
72 71 imp 
 |-  ( ( A e. On /\ ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) ) -> ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) ~<_ ( aleph ` A ) )
73 domtr 
 |-  ( ( ( aleph ` suc A ) ~<_ ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) /\ ( ( cf ` ( aleph ` suc A ) ) X. ( aleph ` A ) ) ~<_ ( aleph ` A ) ) -> ( aleph ` suc A ) ~<_ ( aleph ` A ) )
74 56 72 73 syl2anc 
 |-  ( ( A e. On /\ ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) ) -> ( aleph ` suc A ) ~<_ ( aleph ` A ) )
75 domnsym 
 |-  ( ( aleph ` suc A ) ~<_ ( aleph ` A ) -> -. ( aleph ` A ) ~< ( aleph ` suc A ) )
76 74 75 syl 
 |-  ( ( A e. On /\ ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) ) -> -. ( aleph ` A ) ~< ( aleph ` suc A ) )
77 76 ex 
 |-  ( A e. On -> ( ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) -> -. ( aleph ` A ) ~< ( aleph ` suc A ) ) )
78 1 77 mt2d 
 |-  ( A e. On -> -. ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) )
79 cfon 
 |-  ( cf ` ( aleph ` suc A ) ) e. On
80 cfle 
 |-  ( cf ` ( aleph ` suc A ) ) C_ ( aleph ` suc A )
81 onsseleq 
 |-  ( ( ( cf ` ( aleph ` suc A ) ) e. On /\ ( aleph ` suc A ) e. On ) -> ( ( cf ` ( aleph ` suc A ) ) C_ ( aleph ` suc A ) <-> ( ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) \/ ( cf ` ( aleph ` suc A ) ) = ( aleph ` suc A ) ) ) )
82 80 81 mpbii 
 |-  ( ( ( cf ` ( aleph ` suc A ) ) e. On /\ ( aleph ` suc A ) e. On ) -> ( ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) \/ ( cf ` ( aleph ` suc A ) ) = ( aleph ` suc A ) ) )
83 79 2 82 mp2an 
 |-  ( ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) \/ ( cf ` ( aleph ` suc A ) ) = ( aleph ` suc A ) )
84 83 ori 
 |-  ( -. ( cf ` ( aleph ` suc A ) ) e. ( aleph ` suc A ) -> ( cf ` ( aleph ` suc A ) ) = ( aleph ` suc A ) )
85 78 84 syl 
 |-  ( A e. On -> ( cf ` ( aleph ` suc A ) ) = ( aleph ` suc A ) )
86 cf0 
 |-  ( cf ` (/) ) = (/)
87 alephfnon 
 |-  aleph Fn On
88 87 fndmi 
 |-  dom aleph = On
89 88 eleq2i 
 |-  ( suc A e. dom aleph <-> suc A e. On )
90 onsucb 
 |-  ( A e. On <-> suc A e. On )
91 89 90 bitr4i 
 |-  ( suc A e. dom aleph <-> A e. On )
92 ndmfv 
 |-  ( -. suc A e. dom aleph -> ( aleph ` suc A ) = (/) )
93 91 92 sylnbir 
 |-  ( -. A e. On -> ( aleph ` suc A ) = (/) )
94 93 fveq2d 
 |-  ( -. A e. On -> ( cf ` ( aleph ` suc A ) ) = ( cf ` (/) ) )
95 86 94 93 3eqtr4a 
 |-  ( -. A e. On -> ( cf ` ( aleph ` suc A ) ) = ( aleph ` suc A ) )
96 85 95 pm2.61i 
 |-  ( cf ` ( aleph ` suc A ) ) = ( aleph ` suc A )