Step | Hyp | Ref
| Expression |
1 | | sseq2 3971 |
. . . . . . . . . . 11
β’
((cardβπ΄) =
suc π₯ β (Ο
β (cardβπ΄)
β Ο β suc π₯)) |
2 | 1 | biimpd 228 |
. . . . . . . . . 10
β’
((cardβπ΄) =
suc π₯ β (Ο
β (cardβπ΄)
β Ο β suc π₯)) |
3 | | limom 7819 |
. . . . . . . . . . . 12
β’ Lim
Ο |
4 | | limsssuc 7787 |
. . . . . . . . . . . 12
β’ (Lim
Ο β (Ο β π₯ β Ο β suc π₯)) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . . . 11
β’ (Ο
β π₯ β Ο
β suc π₯) |
6 | | infensuc 9102 |
. . . . . . . . . . . 12
β’ ((π₯ β On β§ Ο β
π₯) β π₯ β suc π₯) |
7 | 6 | ex 414 |
. . . . . . . . . . 11
β’ (π₯ β On β (Ο
β π₯ β π₯ β suc π₯)) |
8 | 5, 7 | biimtrrid 242 |
. . . . . . . . . 10
β’ (π₯ β On β (Ο
β suc π₯ β π₯ β suc π₯)) |
9 | 2, 8 | sylan9r 510 |
. . . . . . . . 9
β’ ((π₯ β On β§
(cardβπ΄) = suc π₯) β (Ο β
(cardβπ΄) β π₯ β suc π₯)) |
10 | | breq2 5110 |
. . . . . . . . . 10
β’
((cardβπ΄) =
suc π₯ β (π₯ β (cardβπ΄) β π₯ β suc π₯)) |
11 | 10 | adantl 483 |
. . . . . . . . 9
β’ ((π₯ β On β§
(cardβπ΄) = suc π₯) β (π₯ β (cardβπ΄) β π₯ β suc π₯)) |
12 | 9, 11 | sylibrd 259 |
. . . . . . . 8
β’ ((π₯ β On β§
(cardβπ΄) = suc π₯) β (Ο β
(cardβπ΄) β π₯ β (cardβπ΄))) |
13 | 12 | ex 414 |
. . . . . . 7
β’ (π₯ β On β
((cardβπ΄) = suc π₯ β (Ο β
(cardβπ΄) β π₯ β (cardβπ΄)))) |
14 | 13 | com3r 87 |
. . . . . 6
β’ (Ο
β (cardβπ΄)
β (π₯ β On β
((cardβπ΄) = suc π₯ β π₯ β (cardβπ΄)))) |
15 | 14 | imp 408 |
. . . . 5
β’ ((Ο
β (cardβπ΄)
β§ π₯ β On) β
((cardβπ΄) = suc π₯ β π₯ β (cardβπ΄))) |
16 | | vex 3448 |
. . . . . . . . . 10
β’ π₯ β V |
17 | 16 | sucid 6400 |
. . . . . . . . 9
β’ π₯ β suc π₯ |
18 | | eleq2 2823 |
. . . . . . . . 9
β’
((cardβπ΄) =
suc π₯ β (π₯ β (cardβπ΄) β π₯ β suc π₯)) |
19 | 17, 18 | mpbiri 258 |
. . . . . . . 8
β’
((cardβπ΄) =
suc π₯ β π₯ β (cardβπ΄)) |
20 | | cardidm 9900 |
. . . . . . . 8
β’
(cardβ(cardβπ΄)) = (cardβπ΄) |
21 | 19, 20 | eleqtrrdi 2845 |
. . . . . . 7
β’
((cardβπ΄) =
suc π₯ β π₯ β
(cardβ(cardβπ΄))) |
22 | | cardne 9906 |
. . . . . . 7
β’ (π₯ β
(cardβ(cardβπ΄))
β Β¬ π₯ β
(cardβπ΄)) |
23 | 21, 22 | syl 17 |
. . . . . 6
β’
((cardβπ΄) =
suc π₯ β Β¬ π₯ β (cardβπ΄)) |
24 | 23 | a1i 11 |
. . . . 5
β’ ((Ο
β (cardβπ΄)
β§ π₯ β On) β
((cardβπ΄) = suc π₯ β Β¬ π₯ β (cardβπ΄))) |
25 | 15, 24 | pm2.65d 195 |
. . . 4
β’ ((Ο
β (cardβπ΄)
β§ π₯ β On) β
Β¬ (cardβπ΄) = suc
π₯) |
26 | 25 | nrexdv 3143 |
. . 3
β’ (Ο
β (cardβπ΄)
β Β¬ βπ₯
β On (cardβπ΄) =
suc π₯) |
27 | | peano1 7826 |
. . . . . 6
β’ β
β Ο |
28 | | ssel 3938 |
. . . . . 6
β’ (Ο
β (cardβπ΄)
β (β
β Ο β β
β (cardβπ΄))) |
29 | 27, 28 | mpi 20 |
. . . . 5
β’ (Ο
β (cardβπ΄)
β β
β (cardβπ΄)) |
30 | | n0i 4294 |
. . . . 5
β’ (β
β (cardβπ΄)
β Β¬ (cardβπ΄)
= β
) |
31 | | cardon 9885 |
. . . . . . . . 9
β’
(cardβπ΄)
β On |
32 | 31 | onordi 6429 |
. . . . . . . 8
β’ Ord
(cardβπ΄) |
33 | | ordzsl 7782 |
. . . . . . . 8
β’ (Ord
(cardβπ΄) β
((cardβπ΄) = β
β¨ βπ₯ β On
(cardβπ΄) = suc π₯ β¨ Lim (cardβπ΄))) |
34 | 32, 33 | mpbi 229 |
. . . . . . 7
β’
((cardβπ΄) =
β
β¨ βπ₯
β On (cardβπ΄) =
suc π₯ β¨ Lim
(cardβπ΄)) |
35 | | 3orass 1091 |
. . . . . . 7
β’
(((cardβπ΄) =
β
β¨ βπ₯
β On (cardβπ΄) =
suc π₯ β¨ Lim
(cardβπ΄)) β
((cardβπ΄) = β
β¨ (βπ₯ β On
(cardβπ΄) = suc π₯ β¨ Lim (cardβπ΄)))) |
36 | 34, 35 | mpbi 229 |
. . . . . 6
β’
((cardβπ΄) =
β
β¨ (βπ₯
β On (cardβπ΄) =
suc π₯ β¨ Lim
(cardβπ΄))) |
37 | 36 | ori 860 |
. . . . 5
β’ (Β¬
(cardβπ΄) = β
β (βπ₯ β On
(cardβπ΄) = suc π₯ β¨ Lim (cardβπ΄))) |
38 | 29, 30, 37 | 3syl 18 |
. . . 4
β’ (Ο
β (cardβπ΄)
β (βπ₯ β On
(cardβπ΄) = suc π₯ β¨ Lim (cardβπ΄))) |
39 | 38 | ord 863 |
. . 3
β’ (Ο
β (cardβπ΄)
β (Β¬ βπ₯
β On (cardβπ΄) =
suc π₯ β Lim
(cardβπ΄))) |
40 | 26, 39 | mpd 15 |
. 2
β’ (Ο
β (cardβπ΄)
β Lim (cardβπ΄)) |
41 | | limomss 7808 |
. 2
β’ (Lim
(cardβπ΄) β
Ο β (cardβπ΄)) |
42 | 40, 41 | impbii 208 |
1
β’ (Ο
β (cardβπ΄)
β Lim (cardβπ΄)) |