Step | Hyp | Ref
| Expression |
1 | | winacard 10635 |
. . . 4
β’ (π΄ β Inaccw β
(cardβπ΄) = π΄) |
2 | | winainf 10637 |
. . . . 5
β’ (π΄ β Inaccw β
Ο β π΄) |
3 | | cardalephex 10033 |
. . . . 5
β’ (Ο
β π΄ β
((cardβπ΄) = π΄ β βπ₯ β On π΄ = (β΅βπ₯))) |
4 | 2, 3 | syl 17 |
. . . 4
β’ (π΄ β Inaccw β
((cardβπ΄) = π΄ β βπ₯ β On π΄ = (β΅βπ₯))) |
5 | 1, 4 | mpbid 231 |
. . 3
β’ (π΄ β Inaccw β
βπ₯ β On π΄ = (β΅βπ₯)) |
6 | 5 | adantr 482 |
. 2
β’ ((π΄ β Inaccw β§
π΄ β Ο) β
βπ₯ β On π΄ = (β΅βπ₯)) |
7 | | df-rex 3075 |
. . 3
β’
(βπ₯ β On
π΄ = (β΅βπ₯) β βπ₯(π₯ β On β§ π΄ = (β΅βπ₯))) |
8 | | simprr 772 |
. . . . . . 7
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β π΄ = (β΅βπ₯)) |
9 | 8 | eqcomd 2743 |
. . . . . 6
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β (β΅βπ₯) = π΄) |
10 | | simprl 770 |
. . . . . . . 8
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β π₯ β On) |
11 | | onzsl 7787 |
. . . . . . . 8
β’ (π₯ β On β (π₯ = β
β¨ βπ¦ β On π₯ = suc π¦ β¨ (π₯ β V β§ Lim π₯))) |
12 | 10, 11 | sylib 217 |
. . . . . . 7
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β (π₯ = β
β¨ βπ¦ β On π₯ = suc π¦ β¨ (π₯ β V β§ Lim π₯))) |
13 | | simplr 768 |
. . . . . . . . . 10
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β π΄ β Ο) |
14 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π₯ = β
β
(β΅βπ₯) =
(β΅ββ
)) |
15 | | aleph0 10009 |
. . . . . . . . . . . . . 14
β’
(β΅ββ
) = Ο |
16 | 14, 15 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (π₯ = β
β
(β΅βπ₯) =
Ο) |
17 | | eqtr 2760 |
. . . . . . . . . . . . 13
β’ ((π΄ = (β΅βπ₯) β§ (β΅βπ₯) = Ο) β π΄ = Ο) |
18 | 16, 17 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((π΄ = (β΅βπ₯) β§ π₯ = β
) β π΄ = Ο) |
19 | 18 | ex 414 |
. . . . . . . . . . 11
β’ (π΄ = (β΅βπ₯) β (π₯ = β
β π΄ = Ο)) |
20 | 19 | necon3ad 2957 |
. . . . . . . . . 10
β’ (π΄ = (β΅βπ₯) β (π΄ β Ο β Β¬ π₯ = β
)) |
21 | 8, 13, 20 | sylc 65 |
. . . . . . . . 9
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β Β¬ π₯ = β
) |
22 | 21 | pm2.21d 121 |
. . . . . . . 8
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β (π₯ = β
β Lim π₯)) |
23 | | breq1 5113 |
. . . . . . . . . . . . . 14
β’ (π§ = (β΅βπ¦) β (π§ βΊ π€ β (β΅βπ¦) βΊ π€)) |
24 | 23 | rexbidv 3176 |
. . . . . . . . . . . . 13
β’ (π§ = (β΅βπ¦) β (βπ€ β π΄ π§ βΊ π€ β βπ€ β π΄ (β΅βπ¦) βΊ π€)) |
25 | | elwina 10629 |
. . . . . . . . . . . . . . 15
β’ (π΄ β Inaccw β
(π΄ β β
β§
(cfβπ΄) = π΄ β§ βπ§ β π΄ βπ€ β π΄ π§ βΊ π€)) |
26 | 25 | simp3bi 1148 |
. . . . . . . . . . . . . 14
β’ (π΄ β Inaccw β
βπ§ β π΄ βπ€ β π΄ π§ βΊ π€) |
27 | 26 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β βπ§ β π΄ βπ€ β π΄ π§ βΊ π€) |
28 | | onsuc 7751 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β On β suc π¦ β On) |
29 | | vex 3452 |
. . . . . . . . . . . . . . . . 17
β’ π¦ β V |
30 | 29 | sucid 6404 |
. . . . . . . . . . . . . . . 16
β’ π¦ β suc π¦ |
31 | | alephord2i 10020 |
. . . . . . . . . . . . . . . 16
β’ (suc
π¦ β On β (π¦ β suc π¦ β (β΅βπ¦) β (β΅βsuc π¦))) |
32 | 28, 30, 31 | mpisyl 21 |
. . . . . . . . . . . . . . 15
β’ (π¦ β On β
(β΅βπ¦) β
(β΅βsuc π¦)) |
33 | 32 | ad2antrl 727 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (β΅βπ¦) β (β΅βsuc π¦)) |
34 | | simplrr 777 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β π΄ = (β΅βπ₯)) |
35 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = suc π¦ β (β΅βπ₯) = (β΅βsuc π¦)) |
36 | 35 | ad2antll 728 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (β΅βπ₯) = (β΅βsuc π¦)) |
37 | 34, 36 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β π΄ = (β΅βsuc π¦)) |
38 | 33, 37 | eleqtrrd 2841 |
. . . . . . . . . . . . 13
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (β΅βπ¦) β π΄) |
39 | 24, 27, 38 | rspcdva 3585 |
. . . . . . . . . . . 12
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β βπ€ β π΄ (β΅βπ¦) βΊ π€) |
40 | 39 | expr 458 |
. . . . . . . . . . 11
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ π¦ β On) β (π₯ = suc π¦ β βπ€ β π΄ (β΅βπ¦) βΊ π€)) |
41 | | iscard 9918 |
. . . . . . . . . . . . . . . . . . 19
β’
((cardβπ΄) =
π΄ β (π΄ β On β§ βπ€ β π΄ π€ βΊ π΄)) |
42 | 41 | simprbi 498 |
. . . . . . . . . . . . . . . . . 18
β’
((cardβπ΄) =
π΄ β βπ€ β π΄ π€ βΊ π΄) |
43 | | rsp 3233 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ€ β
π΄ π€ βΊ π΄ β (π€ β π΄ β π€ βΊ π΄)) |
44 | 1, 42, 43 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β Inaccw β
(π€ β π΄ β π€ βΊ π΄)) |
45 | 44 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (π€ β π΄ β π€ βΊ π΄)) |
46 | 37 | breq2d 5122 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (π€ βΊ π΄ β π€ βΊ (β΅βsuc π¦))) |
47 | 45, 46 | sylibd 238 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (π€ β π΄ β π€ βΊ (β΅βsuc π¦))) |
48 | | alephnbtwn2 10015 |
. . . . . . . . . . . . . . . 16
β’ Β¬
((β΅βπ¦) βΊ
π€ β§ π€ βΊ (β΅βsuc π¦)) |
49 | | pm3.21 473 |
. . . . . . . . . . . . . . . 16
β’ (π€ βΊ (β΅βsuc
π¦) β
((β΅βπ¦) βΊ
π€ β
((β΅βπ¦) βΊ
π€ β§ π€ βΊ (β΅βsuc π¦)))) |
50 | 48, 49 | mtoi 198 |
. . . . . . . . . . . . . . 15
β’ (π€ βΊ (β΅βsuc
π¦) β Β¬
(β΅βπ¦) βΊ
π€) |
51 | 47, 50 | syl6 35 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β (π€ β π΄ β Β¬ (β΅βπ¦) βΊ π€)) |
52 | 51 | imp 408 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
Inaccw β§ π΄
β Ο) β§ (π₯
β On β§ π΄ =
(β΅βπ₯))) β§
(π¦ β On β§ π₯ = suc π¦)) β§ π€ β π΄) β Β¬ (β΅βπ¦) βΊ π€) |
53 | 52 | nrexdv 3147 |
. . . . . . . . . . . 12
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ (π¦ β On β§ π₯ = suc π¦)) β Β¬ βπ€ β π΄ (β΅βπ¦) βΊ π€) |
54 | 53 | expr 458 |
. . . . . . . . . . 11
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ π¦ β On) β (π₯ = suc π¦ β Β¬ βπ€ β π΄ (β΅βπ¦) βΊ π€)) |
55 | 40, 54 | pm2.65d 195 |
. . . . . . . . . 10
β’ ((((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β§ π¦ β On) β Β¬ π₯ = suc π¦) |
56 | 55 | nrexdv 3147 |
. . . . . . . . 9
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β Β¬ βπ¦ β On π₯ = suc π¦) |
57 | 56 | pm2.21d 121 |
. . . . . . . 8
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β (βπ¦ β On π₯ = suc π¦ β Lim π₯)) |
58 | | simpr 486 |
. . . . . . . . 9
β’ ((π₯ β V β§ Lim π₯) β Lim π₯) |
59 | 58 | a1i 11 |
. . . . . . . 8
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β ((π₯ β V β§ Lim π₯) β Lim π₯)) |
60 | 22, 57, 59 | 3jaod 1429 |
. . . . . . 7
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β ((π₯ = β
β¨ βπ¦ β On π₯ = suc π¦ β¨ (π₯ β V β§ Lim π₯)) β Lim π₯)) |
61 | 12, 60 | mpd 15 |
. . . . . 6
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β Lim π₯) |
62 | 9, 61 | jca 513 |
. . . . 5
β’ (((π΄ β Inaccw β§
π΄ β Ο) β§
(π₯ β On β§ π΄ = (β΅βπ₯))) β ((β΅βπ₯) = π΄ β§ Lim π₯)) |
63 | 62 | ex 414 |
. . . 4
β’ ((π΄ β Inaccw β§
π΄ β Ο) β
((π₯ β On β§ π΄ = (β΅βπ₯)) β ((β΅βπ₯) = π΄ β§ Lim π₯))) |
64 | 63 | eximdv 1921 |
. . 3
β’ ((π΄ β Inaccw β§
π΄ β Ο) β
(βπ₯(π₯ β On β§ π΄ = (β΅βπ₯)) β βπ₯((β΅βπ₯) = π΄ β§ Lim π₯))) |
65 | 7, 64 | biimtrid 241 |
. 2
β’ ((π΄ β Inaccw β§
π΄ β Ο) β
(βπ₯ β On π΄ = (β΅βπ₯) β βπ₯((β΅βπ₯) = π΄ β§ Lim π₯))) |
66 | 6, 65 | mpd 15 |
1
β’ ((π΄ β Inaccw β§
π΄ β Ο) β
βπ₯((β΅βπ₯) = π΄ β§ Lim π₯)) |