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 suc A = suc A

Proof

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