Step | Hyp | Ref
| Expression |
1 | | sseq2 4007 |
. . . . . . . . . . 11
β’
((cardβπ΄) =
suc π₯ β (Ο
β (cardβπ΄)
β Ο β suc π₯)) |
2 | 1 | biimpd 228 |
. . . . . . . . . 10
β’
((cardβπ΄) =
suc π₯ β (Ο
β (cardβπ΄)
β Ο β suc π₯)) |
3 | | limom 7867 |
. . . . . . . . . . . 12
β’ Lim
Ο |
4 | | limsssuc 7835 |
. . . . . . . . . . . 12
β’ (Lim
Ο β (Ο β π₯ β Ο β suc π₯)) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . . . 11
β’ (Ο
β π₯ β Ο
β suc π₯) |
6 | | infensuc 9151 |
. . . . . . . . . . . 12
β’ ((π₯ β On β§ Ο β
π₯) β π₯ β suc π₯) |
7 | 6 | ex 413 |
. . . . . . . . . . 11
β’ (π₯ β On β (Ο
β π₯ β π₯ β suc π₯)) |
8 | 5, 7 | biimtrrid 242 |
. . . . . . . . . 10
β’ (π₯ β On β (Ο
β suc π₯ β π₯ β suc π₯)) |
9 | 2, 8 | sylan9r 509 |
. . . . . . . . 9
β’ ((π₯ β On β§
(cardβπ΄) = suc π₯) β (Ο β
(cardβπ΄) β π₯ β suc π₯)) |
10 | | breq2 5151 |
. . . . . . . . . 10
β’
((cardβπ΄) =
suc π₯ β (π₯ β (cardβπ΄) β π₯ β suc π₯)) |
11 | 10 | adantl 482 |
. . . . . . . . 9
β’ ((π₯ β On β§
(cardβπ΄) = suc π₯) β (π₯ β (cardβπ΄) β π₯ β suc π₯)) |
12 | 9, 11 | sylibrd 258 |
. . . . . . . 8
β’ ((π₯ β On β§
(cardβπ΄) = suc π₯) β (Ο β
(cardβπ΄) β π₯ β (cardβπ΄))) |
13 | 12 | ex 413 |
. . . . . . 7
β’ (π₯ β On β
((cardβπ΄) = suc π₯ β (Ο β
(cardβπ΄) β π₯ β (cardβπ΄)))) |
14 | 13 | com3r 87 |
. . . . . 6
β’ (Ο
β (cardβπ΄)
β (π₯ β On β
((cardβπ΄) = suc π₯ β π₯ β (cardβπ΄)))) |
15 | 14 | imp 407 |
. . . . 5
β’ ((Ο
β (cardβπ΄)
β§ π₯ β On) β
((cardβπ΄) = suc π₯ β π₯ β (cardβπ΄))) |
16 | | vex 3478 |
. . . . . . . . . 10
β’ π₯ β V |
17 | 16 | sucid 6443 |
. . . . . . . . 9
β’ π₯ β suc π₯ |
18 | | eleq2 2822 |
. . . . . . . . 9
β’
((cardβπ΄) =
suc π₯ β (π₯ β (cardβπ΄) β π₯ β suc π₯)) |
19 | 17, 18 | mpbiri 257 |
. . . . . . . 8
β’
((cardβπ΄) =
suc π₯ β π₯ β (cardβπ΄)) |
20 | | cardidm 9950 |
. . . . . . . 8
β’
(cardβ(cardβπ΄)) = (cardβπ΄) |
21 | 19, 20 | eleqtrrdi 2844 |
. . . . . . 7
β’
((cardβπ΄) =
suc π₯ β π₯ β
(cardβ(cardβπ΄))) |
22 | | cardne 9956 |
. . . . . . 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 3149 |
. . 3
β’ (Ο
β (cardβπ΄)
β Β¬ βπ₯
β On (cardβπ΄) =
suc π₯) |
27 | | peano1 7875 |
. . . . . 6
β’ β
β Ο |
28 | | ssel 3974 |
. . . . . 6
β’ (Ο
β (cardβπ΄)
β (β
β Ο β β
β (cardβπ΄))) |
29 | 27, 28 | mpi 20 |
. . . . 5
β’ (Ο
β (cardβπ΄)
β β
β (cardβπ΄)) |
30 | | n0i 4332 |
. . . . 5
β’ (β
β (cardβπ΄)
β Β¬ (cardβπ΄)
= β
) |
31 | | cardon 9935 |
. . . . . . . . 9
β’
(cardβπ΄)
β On |
32 | 31 | onordi 6472 |
. . . . . . . 8
β’ Ord
(cardβπ΄) |
33 | | ordzsl 7830 |
. . . . . . . 8
β’ (Ord
(cardβπ΄) β
((cardβπ΄) = β
β¨ βπ₯ β On
(cardβπ΄) = suc π₯ β¨ Lim (cardβπ΄))) |
34 | 32, 33 | mpbi 229 |
. . . . . . 7
β’
((cardβπ΄) =
β
β¨ βπ₯
β On (cardβπ΄) =
suc π₯ β¨ Lim
(cardβπ΄)) |
35 | | 3orass 1090 |
. . . . . . 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 859 |
. . . . 5
β’ (Β¬
(cardβπ΄) = β
β (βπ₯ β On
(cardβπ΄) = suc π₯ β¨ Lim (cardβπ΄))) |
38 | 29, 30, 37 | 3syl 18 |
. . . 4
β’ (Ο
β (cardβπ΄)
β (βπ₯ β On
(cardβπ΄) = suc π₯ β¨ Lim (cardβπ΄))) |
39 | 38 | ord 862 |
. . 3
β’ (Ο
β (cardβπ΄)
β (Β¬ βπ₯
β On (cardβπ΄) =
suc π₯ β Lim
(cardβπ΄))) |
40 | 26, 39 | mpd 15 |
. 2
β’ (Ο
β (cardβπ΄)
β Lim (cardβπ΄)) |
41 | | limomss 7856 |
. 2
β’ (Lim
(cardβπ΄) β
Ο β (cardβπ΄)) |
42 | 40, 41 | impbii 208 |
1
β’ (Ο
β (cardβπ΄)
β Lim (cardβπ΄)) |