Step | Hyp | Ref
| Expression |
1 | | winacard 10690 |
. . . 4
β’ (π΄ β Inaccw β
(cardβπ΄) = π΄) |
2 | | winainf 10692 |
. . . . 5
β’ (π΄ β Inaccw β
Ο β π΄) |
3 | | cardalephex 10088 |
. . . . 5
β’ (Ο
β π΄ β
((cardβπ΄) = π΄ β βπ₯ β On π΄ = (β΅βπ₯))) |
4 | 2, 3 | syl 17 |
. . . 4
β’ (π΄ β Inaccw β
((cardβπ΄) = π΄ β βπ₯ β On π΄ = (β΅βπ₯))) |
5 | 1, 4 | mpbid 231 |
. . 3
β’ (π΄ β Inaccw β
βπ₯ β On π΄ = (β΅βπ₯)) |
6 | 5 | adantr 480 |
. 2
β’ ((π΄ β Inaccw β§
π΄ β Ο) β
βπ₯ β On π΄ = (β΅βπ₯)) |
7 | | df-rex 3070 |
. . 3
β’
(βπ₯ β On
π΄ = (β΅βπ₯) β βπ₯(π₯ β On β§ π΄ = (β΅βπ₯))) |
8 | | simprr 770 |
. . . . . . 7
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β π΄ = (β΅βπ₯)) |
9 | 8 | eqcomd 2737 |
. . . . . 6
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β (β΅βπ₯) = π΄) |
10 | | simprl 768 |
. . . . . . . 8
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β π₯ β On) |
11 | | onzsl 7838 |
. . . . . . . 8
β’ (π₯ β On β (π₯ = β
β¨ βπ¦ β On π₯ = suc π¦ β¨ (π₯ β V β§ Lim π₯))) |
12 | 10, 11 | sylib 217 |
. . . . . . 7
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β (π₯ = β
β¨ βπ¦ β On π₯ = suc π¦ β¨ (π₯ β V β§ Lim π₯))) |
13 | | simplr 766 |
. . . . . . . . . 10
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β π΄ β Ο) |
14 | | fveq2 6892 |
. . . . . . . . . . . . . 14
β’ (π₯ = β
β
(β΅βπ₯) =
(β΅ββ
)) |
15 | | aleph0 10064 |
. . . . . . . . . . . . . 14
β’
(β΅ββ
) = Ο |
16 | 14, 15 | eqtrdi 2787 |
. . . . . . . . . . . . 13
β’ (π₯ = β
β
(β΅βπ₯) =
Ο) |
17 | | eqtr 2754 |
. . . . . . . . . . . . 13
β’ ((π΄ = (β΅βπ₯) β§ (β΅βπ₯) = Ο) β π΄ = Ο) |
18 | 16, 17 | sylan2 592 |
. . . . . . . . . . . 12
β’ ((π΄ = (β΅βπ₯) β§ π₯ = β
) β π΄ = Ο) |
19 | 18 | ex 412 |
. . . . . . . . . . 11
β’ (π΄ = (β΅βπ₯) β (π₯ = β
β π΄ = Ο)) |
20 | 19 | necon3ad 2952 |
. . . . . . . . . 10
β’ (π΄ = (β΅βπ₯) β (π΄ β Ο β Β¬ π₯ = β
)) |
21 | 8, 13, 20 | sylc 65 |
. . . . . . . . 9
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β Β¬ π₯ = β
) |
22 | 21 | pm2.21d 121 |
. . . . . . . 8
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β (π₯ = β
β Lim π₯)) |
23 | | breq1 5152 |
. . . . . . . . . . . . . 14
β’ (π§ = (β΅βπ¦) β (π§ βΊ π€ β (β΅βπ¦) βΊ π€)) |
24 | 23 | rexbidv 3177 |
. . . . . . . . . . . . 13
β’ (π§ = (β΅βπ¦) β (βπ€ β π΄ π§ βΊ π€ β βπ€ β π΄ (β΅βπ¦) βΊ π€)) |
25 | | elwina 10684 |
. . . . . . . . . . . . . . 15
β’ (π΄ β Inaccw β
(π΄ β β
β§
(cfβπ΄) = π΄ β§ βπ§ β π΄ βπ€ β π΄ π§ βΊ π€)) |
26 | 25 | simp3bi 1146 |
. . . . . . . . . . . . . 14
β’ (π΄ β Inaccw β
βπ§ β π΄ βπ€ β π΄ π§ βΊ π€) |
27 | 26 | ad3antrrr 727 |
. . . . . . . . . . . . 13
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β βπ§ β π΄ βπ€ β π΄ π§ βΊ π€) |
28 | | onsuc 7802 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β On β suc π¦ β On) |
29 | | vex 3477 |
. . . . . . . . . . . . . . . . 17
β’ π¦ β V |
30 | 29 | sucid 6447 |
. . . . . . . . . . . . . . . 16
β’ π¦ β suc π¦ |
31 | | alephord2i 10075 |
. . . . . . . . . . . . . . . 16
β’ (suc
π¦ β On β (π¦ β suc π¦ β (β΅βπ¦) β (β΅βsuc π¦))) |
32 | 28, 30, 31 | mpisyl 21 |
. . . . . . . . . . . . . . 15
β’ (π¦ β On β
(β΅βπ¦) β
(β΅βsuc π¦)) |
33 | 32 | ad2antrl 725 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (β΅βπ¦) β (β΅βsuc π¦)) |
34 | | simplrr 775 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β π΄ = (β΅βπ₯)) |
35 | | fveq2 6892 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = suc π¦ β (β΅βπ₯) = (β΅βsuc π¦)) |
36 | 35 | ad2antll 726 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (β΅βπ₯) = (β΅βsuc π¦)) |
37 | 34, 36 | eqtrd 2771 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β π΄ = (β΅βsuc π¦)) |
38 | 33, 37 | eleqtrrd 2835 |
. . . . . . . . . . . . 13
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (β΅βπ¦) β π΄) |
39 | 24, 27, 38 | rspcdva 3614 |
. . . . . . . . . . . 12
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β βπ€ β π΄ (β΅βπ¦) βΊ π€) |
40 | 39 | expr 456 |
. . . . . . . . . . 11
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ π¦ β On) β (π₯ = suc π¦ β βπ€ β π΄ (β΅βπ¦) βΊ π€)) |
41 | | iscard 9973 |
. . . . . . . . . . . . . . . . . . 19
β’
((cardβπ΄) =
π΄ β (π΄ β On β§ βπ€ β π΄ π€ βΊ π΄)) |
42 | 41 | simprbi 496 |
. . . . . . . . . . . . . . . . . 18
β’
((cardβπ΄) =
π΄ β βπ€ β π΄ π€ βΊ π΄) |
43 | | rsp 3243 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ€ β
π΄ π€ βΊ π΄ β (π€ β π΄ β π€ βΊ π΄)) |
44 | 1, 42, 43 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β Inaccw β
(π€ β π΄ β π€ βΊ π΄)) |
45 | 44 | ad3antrrr 727 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (π€ β π΄ β π€ βΊ π΄)) |
46 | 37 | breq2d 5161 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (π€ βΊ π΄ β π€ βΊ (β΅βsuc π¦))) |
47 | 45, 46 | sylibd 238 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (π€ β π΄ β π€ βΊ (β΅βsuc π¦))) |
48 | | alephnbtwn2 10070 |
. . . . . . . . . . . . . . . 16
β’ Β¬
((β΅βπ¦) βΊ
π€ β§ π€ βΊ (β΅βsuc π¦)) |
49 | | pm3.21 471 |
. . . . . . . . . . . . . . . 16
β’ (π€ βΊ (β΅βsuc
π¦) β
((β΅βπ¦) βΊ
π€ β
((β΅βπ¦) βΊ
π€ β§ π€ βΊ (β΅βsuc π¦)))) |
50 | 48, 49 | mtoi 198 |
. . . . . . . . . . . . . . 15
β’ (π€ βΊ (β΅βsuc
π¦) β Β¬
(β΅βπ¦) βΊ
π€) |
51 | 47, 50 | syl6 35 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (π€ β π΄ β Β¬ (β΅βπ¦) βΊ π€)) |
52 | 51 | imp 406 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
Inaccw β§ π΄
β Ο) β§ (π₯
β On β§ π΄ =
(β΅βπ₯))) β§
(π¦ β On β§ π₯ = suc π¦)) β§ π€ β π΄) β Β¬ (β΅βπ¦) βΊ π€) |
53 | 52 | nrexdv 3148 |
. . . . . . . . . . . 12
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β Β¬ βπ€ β π΄ (β΅βπ¦) βΊ π€) |
54 | 53 | expr 456 |
. . . . . . . . . . 11
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ π¦ β On) β (π₯ = suc π¦ β Β¬ βπ€ β π΄ (β΅βπ¦) βΊ π€)) |
55 | 40, 54 | pm2.65d 195 |
. . . . . . . . . 10
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ π¦ β On) β Β¬ π₯ = suc π¦) |
56 | 55 | nrexdv 3148 |
. . . . . . . . 9
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β Β¬ βπ¦ β On π₯ = suc π¦) |
57 | 56 | pm2.21d 121 |
. . . . . . . 8
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β (βπ¦ β On π₯ = suc π¦ β Lim π₯)) |
58 | | simpr 484 |
. . . . . . . . 9
β’ ((π₯ β V β§ Lim π₯) β Lim π₯) |
59 | 58 | a1i 11 |
. . . . . . . 8
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β ((π₯ β V β§ Lim π₯) β Lim π₯)) |
60 | 22, 57, 59 | 3jaod 1427 |
. . . . . . 7
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β ((π₯ = β
β¨ βπ¦ β On π₯ = suc π¦ β¨ (π₯ β V β§ Lim π₯)) β Lim π₯)) |
61 | 12, 60 | mpd 15 |
. . . . . 6
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β Lim π₯) |
62 | 9, 61 | jca 511 |
. . . . 5
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β ((β΅βπ₯) = π΄ β§ Lim π₯)) |
63 | 62 | ex 412 |
. . . 4
β’ ((π΄ β Inaccw β§
π΄ β Ο) β
((π₯ β On β§ π΄ = (β΅βπ₯)) β ((β΅βπ₯) = π΄ β§ Lim π₯))) |
64 | 63 | eximdv 1919 |
. . 3
β’ ((π΄ β Inaccw β§
π΄ β Ο) β
(βπ₯(π₯ β On β§ π΄ = (β΅βπ₯)) β βπ₯((β΅βπ₯) = π΄ β§ Lim π₯))) |
65 | 7, 64 | biimtrid 241 |
. 2
β’ ((π΄ β Inaccw β§
π΄ β Ο) β
(βπ₯ β On π΄ = (β΅βπ₯) β βπ₯((β΅βπ₯) = π΄ β§ Lim π₯))) |
66 | 6, 65 | mpd 15 |
1
β’ ((π΄ β Inaccw β§
π΄ β Ο) β
βπ₯((β΅βπ₯) = π΄ β§ Lim π₯)) |