Step | Hyp | Ref
| Expression |
1 | | cardne 9906 |
. . . . 5
β’
((cardβπ΅)
β (cardβπ΄)
β Β¬ (cardβπ΅)
β π΄) |
2 | | ennum 9888 |
. . . . . . . 8
β’ (π΄ β π΅ β (π΄ β dom card β π΅ β dom card)) |
3 | 2 | biimpa 478 |
. . . . . . 7
β’ ((π΄ β π΅ β§ π΄ β dom card) β π΅ β dom card) |
4 | | cardid2 9894 |
. . . . . . 7
β’ (π΅ β dom card β
(cardβπ΅) β
π΅) |
5 | 3, 4 | syl 17 |
. . . . . 6
β’ ((π΄ β π΅ β§ π΄ β dom card) β (cardβπ΅) β π΅) |
6 | | ensym 8946 |
. . . . . . 7
β’ (π΄ β π΅ β π΅ β π΄) |
7 | 6 | adantr 482 |
. . . . . 6
β’ ((π΄ β π΅ β§ π΄ β dom card) β π΅ β π΄) |
8 | | entr 8949 |
. . . . . 6
β’
(((cardβπ΅)
β π΅ β§ π΅ β π΄) β (cardβπ΅) β π΄) |
9 | 5, 7, 8 | syl2anc 585 |
. . . . 5
β’ ((π΄ β π΅ β§ π΄ β dom card) β (cardβπ΅) β π΄) |
10 | 1, 9 | nsyl3 138 |
. . . 4
β’ ((π΄ β π΅ β§ π΄ β dom card) β Β¬
(cardβπ΅) β
(cardβπ΄)) |
11 | | cardon 9885 |
. . . . 5
β’
(cardβπ΄)
β On |
12 | | cardon 9885 |
. . . . 5
β’
(cardβπ΅)
β On |
13 | | ontri1 6352 |
. . . . 5
β’
(((cardβπ΄)
β On β§ (cardβπ΅) β On) β ((cardβπ΄) β (cardβπ΅) β Β¬ (cardβπ΅) β (cardβπ΄))) |
14 | 11, 12, 13 | mp2an 691 |
. . . 4
β’
((cardβπ΄)
β (cardβπ΅)
β Β¬ (cardβπ΅)
β (cardβπ΄)) |
15 | 10, 14 | sylibr 233 |
. . 3
β’ ((π΄ β π΅ β§ π΄ β dom card) β (cardβπ΄) β (cardβπ΅)) |
16 | | cardne 9906 |
. . . . 5
β’
((cardβπ΄)
β (cardβπ΅)
β Β¬ (cardβπ΄)
β π΅) |
17 | | cardid2 9894 |
. . . . . 6
β’ (π΄ β dom card β
(cardβπ΄) β
π΄) |
18 | | id 22 |
. . . . . 6
β’ (π΄ β π΅ β π΄ β π΅) |
19 | | entr 8949 |
. . . . . 6
β’
(((cardβπ΄)
β π΄ β§ π΄ β π΅) β (cardβπ΄) β π΅) |
20 | 17, 18, 19 | syl2anr 598 |
. . . . 5
β’ ((π΄ β π΅ β§ π΄ β dom card) β (cardβπ΄) β π΅) |
21 | 16, 20 | nsyl3 138 |
. . . 4
β’ ((π΄ β π΅ β§ π΄ β dom card) β Β¬
(cardβπ΄) β
(cardβπ΅)) |
22 | | ontri1 6352 |
. . . . 5
β’
(((cardβπ΅)
β On β§ (cardβπ΄) β On) β ((cardβπ΅) β (cardβπ΄) β Β¬ (cardβπ΄) β (cardβπ΅))) |
23 | 12, 11, 22 | mp2an 691 |
. . . 4
β’
((cardβπ΅)
β (cardβπ΄)
β Β¬ (cardβπ΄)
β (cardβπ΅)) |
24 | 21, 23 | sylibr 233 |
. . 3
β’ ((π΄ β π΅ β§ π΄ β dom card) β (cardβπ΅) β (cardβπ΄)) |
25 | 15, 24 | eqssd 3962 |
. 2
β’ ((π΄ β π΅ β§ π΄ β dom card) β (cardβπ΄) = (cardβπ΅)) |
26 | | ndmfv 6878 |
. . . 4
β’ (Β¬
π΄ β dom card β
(cardβπ΄) =
β
) |
27 | 26 | adantl 483 |
. . 3
β’ ((π΄ β π΅ β§ Β¬ π΄ β dom card) β (cardβπ΄) = β
) |
28 | 2 | notbid 318 |
. . . . 5
β’ (π΄ β π΅ β (Β¬ π΄ β dom card β Β¬ π΅ β dom
card)) |
29 | 28 | biimpa 478 |
. . . 4
β’ ((π΄ β π΅ β§ Β¬ π΄ β dom card) β Β¬ π΅ β dom
card) |
30 | | ndmfv 6878 |
. . . 4
β’ (Β¬
π΅ β dom card β
(cardβπ΅) =
β
) |
31 | 29, 30 | syl 17 |
. . 3
β’ ((π΄ β π΅ β§ Β¬ π΄ β dom card) β (cardβπ΅) = β
) |
32 | 27, 31 | eqtr4d 2776 |
. 2
β’ ((π΄ β π΅ β§ Β¬ π΄ β dom card) β (cardβπ΄) = (cardβπ΅)) |
33 | 25, 32 | pm2.61dan 812 |
1
β’ (π΄ β π΅ β (cardβπ΄) = (cardβπ΅)) |