Step | Hyp | Ref
| Expression |
1 | | elfvdm 6880 |
. 2
β’ (π΄ β (cardβπ΅) β π΅ β dom card) |
2 | | cardon 9885 |
. . . . . . . . . 10
β’
(cardβπ΅)
β On |
3 | 2 | oneli 6432 |
. . . . . . . . 9
β’ (π΄ β (cardβπ΅) β π΄ β On) |
4 | | breq1 5109 |
. . . . . . . . . 10
β’ (π₯ = π΄ β (π₯ β π΅ β π΄ β π΅)) |
5 | 4 | onintss 6369 |
. . . . . . . . 9
β’ (π΄ β On β (π΄ β π΅ β β© {π₯ β On β£ π₯ β π΅} β π΄)) |
6 | 3, 5 | syl 17 |
. . . . . . . 8
β’ (π΄ β (cardβπ΅) β (π΄ β π΅ β β© {π₯ β On β£ π₯ β π΅} β π΄)) |
7 | 6 | adantl 483 |
. . . . . . 7
β’ ((π΅ β dom card β§ π΄ β (cardβπ΅)) β (π΄ β π΅ β β© {π₯ β On β£ π₯ β π΅} β π΄)) |
8 | | cardval3 9893 |
. . . . . . . . 9
β’ (π΅ β dom card β
(cardβπ΅) = β© {π₯
β On β£ π₯ β
π΅}) |
9 | 8 | sseq1d 3976 |
. . . . . . . 8
β’ (π΅ β dom card β
((cardβπ΅) β
π΄ β β© {π₯
β On β£ π₯ β
π΅} β π΄)) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((π΅ β dom card β§ π΄ β (cardβπ΅)) β ((cardβπ΅) β π΄ β β© {π₯ β On β£ π₯ β π΅} β π΄)) |
11 | 7, 10 | sylibrd 259 |
. . . . . 6
β’ ((π΅ β dom card β§ π΄ β (cardβπ΅)) β (π΄ β π΅ β (cardβπ΅) β π΄)) |
12 | | ontri1 6352 |
. . . . . . . 8
β’
(((cardβπ΅)
β On β§ π΄ β
On) β ((cardβπ΅)
β π΄ β Β¬
π΄ β (cardβπ΅))) |
13 | 2, 3, 12 | sylancr 588 |
. . . . . . 7
β’ (π΄ β (cardβπ΅) β ((cardβπ΅) β π΄ β Β¬ π΄ β (cardβπ΅))) |
14 | 13 | adantl 483 |
. . . . . 6
β’ ((π΅ β dom card β§ π΄ β (cardβπ΅)) β ((cardβπ΅) β π΄ β Β¬ π΄ β (cardβπ΅))) |
15 | 11, 14 | sylibd 238 |
. . . . 5
β’ ((π΅ β dom card β§ π΄ β (cardβπ΅)) β (π΄ β π΅ β Β¬ π΄ β (cardβπ΅))) |
16 | 15 | con2d 134 |
. . . 4
β’ ((π΅ β dom card β§ π΄ β (cardβπ΅)) β (π΄ β (cardβπ΅) β Β¬ π΄ β π΅)) |
17 | 16 | ex 414 |
. . 3
β’ (π΅ β dom card β (π΄ β (cardβπ΅) β (π΄ β (cardβπ΅) β Β¬ π΄ β π΅))) |
18 | 17 | pm2.43d 53 |
. 2
β’ (π΅ β dom card β (π΄ β (cardβπ΅) β Β¬ π΄ β π΅)) |
19 | 1, 18 | mpcom 38 |
1
β’ (π΄ β (cardβπ΅) β Β¬ π΄ β π΅) |