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 ffvelrn
 |-  ( ( 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 suceloni
 |-  ( 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 syl5ibr
 |-  ( 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 syl5ibr
 |-  ( 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 sucelon
 |-  ( 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 )