Step | Hyp | Ref
| Expression |
1 | | alephcard 10067 |
. . . 4
β’
(cardβ(β΅βπ΄)) = (β΅βπ΄) |
2 | 1 | a1i 11 |
. . 3
β’ (π΄ β On β
(cardβ(β΅βπ΄)) = (β΅βπ΄)) |
3 | | alephgeom 10079 |
. . . 4
β’ (π΄ β On β Ο
β (β΅βπ΄)) |
4 | 3 | biimpi 215 |
. . 3
β’ (π΄ β On β Ο
β (β΅βπ΄)) |
5 | | alephord2i 10074 |
. . . . 5
β’ (π΄ β On β (π¦ β π΄ β (β΅βπ¦) β (β΅βπ΄))) |
6 | | elirr 9594 |
. . . . . . 7
β’ Β¬
(β΅βπ¦) β
(β΅βπ¦) |
7 | | eleq2 2822 |
. . . . . . 7
β’
((β΅βπ΄) =
(β΅βπ¦) β
((β΅βπ¦) β
(β΅βπ΄) β
(β΅βπ¦) β
(β΅βπ¦))) |
8 | 6, 7 | mtbiri 326 |
. . . . . 6
β’
((β΅βπ΄) =
(β΅βπ¦) β
Β¬ (β΅βπ¦)
β (β΅βπ΄)) |
9 | 8 | con2i 139 |
. . . . 5
β’
((β΅βπ¦)
β (β΅βπ΄)
β Β¬ (β΅βπ΄) = (β΅βπ¦)) |
10 | 5, 9 | syl6 35 |
. . . 4
β’ (π΄ β On β (π¦ β π΄ β Β¬ (β΅βπ΄) = (β΅βπ¦))) |
11 | 10 | ralrimiv 3145 |
. . 3
β’ (π΄ β On β βπ¦ β π΄ Β¬ (β΅βπ΄) = (β΅βπ¦)) |
12 | | fvex 6904 |
. . . 4
β’
(β΅βπ΄)
β V |
13 | | fveq2 6891 |
. . . . . 6
β’ (π₯ = (β΅βπ΄) β (cardβπ₯) =
(cardβ(β΅βπ΄))) |
14 | | id 22 |
. . . . . 6
β’ (π₯ = (β΅βπ΄) β π₯ = (β΅βπ΄)) |
15 | 13, 14 | eqeq12d 2748 |
. . . . 5
β’ (π₯ = (β΅βπ΄) β ((cardβπ₯) = π₯ β (cardβ(β΅βπ΄)) = (β΅βπ΄))) |
16 | | sseq2 4008 |
. . . . 5
β’ (π₯ = (β΅βπ΄) β (Ο β π₯ β Ο β
(β΅βπ΄))) |
17 | | eqeq1 2736 |
. . . . . . 7
β’ (π₯ = (β΅βπ΄) β (π₯ = (β΅βπ¦) β (β΅βπ΄) = (β΅βπ¦))) |
18 | 17 | notbid 317 |
. . . . . 6
β’ (π₯ = (β΅βπ΄) β (Β¬ π₯ = (β΅βπ¦) β Β¬
(β΅βπ΄) =
(β΅βπ¦))) |
19 | 18 | ralbidv 3177 |
. . . . 5
β’ (π₯ = (β΅βπ΄) β (βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦) β βπ¦ β π΄ Β¬ (β΅βπ΄) = (β΅βπ¦))) |
20 | 15, 16, 19 | 3anbi123d 1436 |
. . . 4
β’ (π₯ = (β΅βπ΄) β (((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦)) β ((cardβ(β΅βπ΄)) = (β΅βπ΄) β§ Ο β
(β΅βπ΄) β§
βπ¦ β π΄ Β¬ (β΅βπ΄) = (β΅βπ¦)))) |
21 | 12, 20 | elab 3668 |
. . 3
β’
((β΅βπ΄)
β {π₯ β£
((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))} β ((cardβ(β΅βπ΄)) = (β΅βπ΄) β§ Ο β
(β΅βπ΄) β§
βπ¦ β π΄ Β¬ (β΅βπ΄) = (β΅βπ¦))) |
22 | 2, 4, 11, 21 | syl3anbrc 1343 |
. 2
β’ (π΄ β On β
(β΅βπ΄) β
{π₯ β£
((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))}) |
23 | | eleq1 2821 |
. . . . . . . . . . . . . . 15
β’ (π§ = (β΅βπ¦) β (π§ β (β΅βπ΄) β (β΅βπ¦) β (β΅βπ΄))) |
24 | | alephord2 10073 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β On β§ π΄ β On) β (π¦ β π΄ β (β΅βπ¦) β (β΅βπ΄))) |
25 | 24 | bicomd 222 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β On β§ π΄ β On) β
((β΅βπ¦) β
(β΅βπ΄) β
π¦ β π΄)) |
26 | 23, 25 | sylan9bbr 511 |
. . . . . . . . . . . . . 14
β’ (((π¦ β On β§ π΄ β On) β§ π§ = (β΅βπ¦)) β (π§ β (β΅βπ΄) β π¦ β π΄)) |
27 | 26 | biimpcd 248 |
. . . . . . . . . . . . 13
β’ (π§ β (β΅βπ΄) β (((π¦ β On β§ π΄ β On) β§ π§ = (β΅βπ¦)) β π¦ β π΄)) |
28 | | simpr 485 |
. . . . . . . . . . . . 13
β’ (((π¦ β On β§ π΄ β On) β§ π§ = (β΅βπ¦)) β π§ = (β΅βπ¦)) |
29 | 27, 28 | jca2 514 |
. . . . . . . . . . . 12
β’ (π§ β (β΅βπ΄) β (((π¦ β On β§ π΄ β On) β§ π§ = (β΅βπ¦)) β (π¦ β π΄ β§ π§ = (β΅βπ¦)))) |
30 | 29 | exp4c 433 |
. . . . . . . . . . 11
β’ (π§ β (β΅βπ΄) β (π¦ β On β (π΄ β On β (π§ = (β΅βπ¦) β (π¦ β π΄ β§ π§ = (β΅βπ¦)))))) |
31 | 30 | com3r 87 |
. . . . . . . . . 10
β’ (π΄ β On β (π§ β (β΅βπ΄) β (π¦ β On β (π§ = (β΅βπ¦) β (π¦ β π΄ β§ π§ = (β΅βπ¦)))))) |
32 | 31 | imp4b 422 |
. . . . . . . . 9
β’ ((π΄ β On β§ π§ β (β΅βπ΄)) β ((π¦ β On β§ π§ = (β΅βπ¦)) β (π¦ β π΄ β§ π§ = (β΅βπ¦)))) |
33 | 32 | reximdv2 3164 |
. . . . . . . 8
β’ ((π΄ β On β§ π§ β (β΅βπ΄)) β (βπ¦ β On π§ = (β΅βπ¦) β βπ¦ β π΄ π§ = (β΅βπ¦))) |
34 | | cardalephex 10087 |
. . . . . . . . 9
β’ (Ο
β π§ β
((cardβπ§) = π§ β βπ¦ β On π§ = (β΅βπ¦))) |
35 | 34 | biimpac 479 |
. . . . . . . 8
β’
(((cardβπ§) =
π§ β§ Ο β
π§) β βπ¦ β On π§ = (β΅βπ¦)) |
36 | 33, 35 | impel 506 |
. . . . . . 7
β’ (((π΄ β On β§ π§ β (β΅βπ΄)) β§ ((cardβπ§) = π§ β§ Ο β π§)) β βπ¦ β π΄ π§ = (β΅βπ¦)) |
37 | | dfrex2 3073 |
. . . . . . 7
β’
(βπ¦ β
π΄ π§ = (β΅βπ¦) β Β¬ βπ¦ β π΄ Β¬ π§ = (β΅βπ¦)) |
38 | 36, 37 | sylib 217 |
. . . . . 6
β’ (((π΄ β On β§ π§ β (β΅βπ΄)) β§ ((cardβπ§) = π§ β§ Ο β π§)) β Β¬ βπ¦ β π΄ Β¬ π§ = (β΅βπ¦)) |
39 | | nan 828 |
. . . . . 6
β’ (((π΄ β On β§ π§ β (β΅βπ΄)) β Β¬
(((cardβπ§) = π§ β§ Ο β π§) β§ βπ¦ β π΄ Β¬ π§ = (β΅βπ¦))) β (((π΄ β On β§ π§ β (β΅βπ΄)) β§ ((cardβπ§) = π§ β§ Ο β π§)) β Β¬ βπ¦ β π΄ Β¬ π§ = (β΅βπ¦))) |
40 | 38, 39 | mpbir 230 |
. . . . 5
β’ ((π΄ β On β§ π§ β (β΅βπ΄)) β Β¬
(((cardβπ§) = π§ β§ Ο β π§) β§ βπ¦ β π΄ Β¬ π§ = (β΅βπ¦))) |
41 | 40 | ex 413 |
. . . 4
β’ (π΄ β On β (π§ β (β΅βπ΄) β Β¬
(((cardβπ§) = π§ β§ Ο β π§) β§ βπ¦ β π΄ Β¬ π§ = (β΅βπ¦)))) |
42 | | vex 3478 |
. . . . . . 7
β’ π§ β V |
43 | | fveq2 6891 |
. . . . . . . . 9
β’ (π₯ = π§ β (cardβπ₯) = (cardβπ§)) |
44 | | id 22 |
. . . . . . . . 9
β’ (π₯ = π§ β π₯ = π§) |
45 | 43, 44 | eqeq12d 2748 |
. . . . . . . 8
β’ (π₯ = π§ β ((cardβπ₯) = π₯ β (cardβπ§) = π§)) |
46 | | sseq2 4008 |
. . . . . . . 8
β’ (π₯ = π§ β (Ο β π₯ β Ο β π§)) |
47 | | eqeq1 2736 |
. . . . . . . . . 10
β’ (π₯ = π§ β (π₯ = (β΅βπ¦) β π§ = (β΅βπ¦))) |
48 | 47 | notbid 317 |
. . . . . . . . 9
β’ (π₯ = π§ β (Β¬ π₯ = (β΅βπ¦) β Β¬ π§ = (β΅βπ¦))) |
49 | 48 | ralbidv 3177 |
. . . . . . . 8
β’ (π₯ = π§ β (βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦) β βπ¦ β π΄ Β¬ π§ = (β΅βπ¦))) |
50 | 45, 46, 49 | 3anbi123d 1436 |
. . . . . . 7
β’ (π₯ = π§ β (((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦)) β ((cardβπ§) = π§ β§ Ο β π§ β§ βπ¦ β π΄ Β¬ π§ = (β΅βπ¦)))) |
51 | 42, 50 | elab 3668 |
. . . . . 6
β’ (π§ β {π₯ β£ ((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))} β ((cardβπ§) = π§ β§ Ο β π§ β§ βπ¦ β π΄ Β¬ π§ = (β΅βπ¦))) |
52 | | df-3an 1089 |
. . . . . 6
β’
(((cardβπ§) =
π§ β§ Ο β
π§ β§ βπ¦ β π΄ Β¬ π§ = (β΅βπ¦)) β (((cardβπ§) = π§ β§ Ο β π§) β§ βπ¦ β π΄ Β¬ π§ = (β΅βπ¦))) |
53 | 51, 52 | bitri 274 |
. . . . 5
β’ (π§ β {π₯ β£ ((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))} β (((cardβπ§) = π§ β§ Ο β π§) β§ βπ¦ β π΄ Β¬ π§ = (β΅βπ¦))) |
54 | 53 | notbii 319 |
. . . 4
β’ (Β¬
π§ β {π₯ β£ ((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))} β Β¬ (((cardβπ§) = π§ β§ Ο β π§) β§ βπ¦ β π΄ Β¬ π§ = (β΅βπ¦))) |
55 | 41, 54 | imbitrrdi 251 |
. . 3
β’ (π΄ β On β (π§ β (β΅βπ΄) β Β¬ π§ β {π₯ β£ ((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))})) |
56 | 55 | ralrimiv 3145 |
. 2
β’ (π΄ β On β βπ§ β (β΅βπ΄) Β¬ π§ β {π₯ β£ ((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))}) |
57 | | cardon 9941 |
. . . . . 6
β’
(cardβπ₯)
β On |
58 | | eleq1 2821 |
. . . . . 6
β’
((cardβπ₯) =
π₯ β ((cardβπ₯) β On β π₯ β On)) |
59 | 57, 58 | mpbii 232 |
. . . . 5
β’
((cardβπ₯) =
π₯ β π₯ β On) |
60 | 59 | 3ad2ant1 1133 |
. . . 4
β’
(((cardβπ₯) =
π₯ β§ Ο β
π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦)) β π₯ β On) |
61 | 60 | abssi 4067 |
. . 3
β’ {π₯ β£ ((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))} β On |
62 | | oneqmini 6416 |
. . 3
β’ ({π₯ β£ ((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))} β On β (((β΅βπ΄) β {π₯ β£ ((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))} β§ βπ§ β (β΅βπ΄) Β¬ π§ β {π₯ β£ ((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))}) β (β΅βπ΄) = β© {π₯ β£ ((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))})) |
63 | 61, 62 | ax-mp 5 |
. 2
β’
(((β΅βπ΄)
β {π₯ β£
((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))} β§ βπ§ β (β΅βπ΄) Β¬ π§ β {π₯ β£ ((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))}) β (β΅βπ΄) = β© {π₯ β£ ((cardβπ₯) = π₯ β§ Ο β π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))}) |
64 | 22, 56, 63 | syl2anc 584 |
1
β’ (π΄ β On β
(β΅βπ΄) = β© {π₯
β£ ((cardβπ₯) =
π₯ β§ Ο β
π₯ β§ βπ¦ β π΄ Β¬ π₯ = (β΅βπ¦))}) |