Step | Hyp | Ref
| Expression |
1 | | cardnueq0 9905 |
. . . . . 6
β’ (π΄ β dom card β
((cardβπ΄) = β
β π΄ =
β
)) |
2 | 1 | adantr 482 |
. . . . 5
β’ ((π΄ β dom card β§ π΅ β π) β ((cardβπ΄) = β
β π΄ = β
)) |
3 | 2 | biimpa 478 |
. . . 4
β’ (((π΄ β dom card β§ π΅ β π) β§ (cardβπ΄) = β
) β π΄ = β
) |
4 | | 0domg 9047 |
. . . . 5
β’ (π΅ β π β β
βΌ π΅) |
5 | 4 | ad2antlr 726 |
. . . 4
β’ (((π΄ β dom card β§ π΅ β π) β§ (cardβπ΄) = β
) β β
βΌ π΅) |
6 | 3, 5 | eqbrtrd 5128 |
. . 3
β’ (((π΄ β dom card β§ π΅ β π) β§ (cardβπ΄) = β
) β π΄ βΌ π΅) |
7 | 6 | a1d 25 |
. 2
β’ (((π΄ β dom card β§ π΅ β π) β§ (cardβπ΄) = β
) β ((cardβπ΄) β (cardβπ΅) β π΄ βΌ π΅)) |
8 | | fvex 6856 |
. . . . 5
β’
(cardβπ΅)
β V |
9 | | simprr 772 |
. . . . 5
β’ (((π΄ β dom card β§ π΅ β π) β§ ((cardβπ΄) β β
β§ (cardβπ΄) β (cardβπ΅))) β (cardβπ΄) β (cardβπ΅)) |
10 | | ssdomg 8943 |
. . . . 5
β’
((cardβπ΅)
β V β ((cardβπ΄) β (cardβπ΅) β (cardβπ΄) βΌ (cardβπ΅))) |
11 | 8, 9, 10 | mpsyl 68 |
. . . 4
β’ (((π΄ β dom card β§ π΅ β π) β§ ((cardβπ΄) β β
β§ (cardβπ΄) β (cardβπ΅))) β (cardβπ΄) βΌ (cardβπ΅)) |
12 | | cardid2 9894 |
. . . . . 6
β’ (π΄ β dom card β
(cardβπ΄) β
π΄) |
13 | 12 | ad2antrr 725 |
. . . . 5
β’ (((π΄ β dom card β§ π΅ β π) β§ ((cardβπ΄) β β
β§ (cardβπ΄) β (cardβπ΅))) β (cardβπ΄) β π΄) |
14 | | simprl 770 |
. . . . . . 7
β’ (((π΄ β dom card β§ π΅ β π) β§ ((cardβπ΄) β β
β§ (cardβπ΄) β (cardβπ΅))) β (cardβπ΄) β β
) |
15 | | ssn0 4361 |
. . . . . . 7
β’
(((cardβπ΄)
β (cardβπ΅)
β§ (cardβπ΄) β
β
) β (cardβπ΅) β β
) |
16 | 9, 14, 15 | syl2anc 585 |
. . . . . 6
β’ (((π΄ β dom card β§ π΅ β π) β§ ((cardβπ΄) β β
β§ (cardβπ΄) β (cardβπ΅))) β (cardβπ΅) β β
) |
17 | | ndmfv 6878 |
. . . . . . 7
β’ (Β¬
π΅ β dom card β
(cardβπ΅) =
β
) |
18 | 17 | necon1ai 2968 |
. . . . . 6
β’
((cardβπ΅) β
β
β π΅ β dom
card) |
19 | | cardid2 9894 |
. . . . . 6
β’ (π΅ β dom card β
(cardβπ΅) β
π΅) |
20 | 16, 18, 19 | 3syl 18 |
. . . . 5
β’ (((π΄ β dom card β§ π΅ β π) β§ ((cardβπ΄) β β
β§ (cardβπ΄) β (cardβπ΅))) β (cardβπ΅) β π΅) |
21 | | domen1 9066 |
. . . . . 6
β’
((cardβπ΄)
β π΄ β
((cardβπ΄) βΌ
(cardβπ΅) β π΄ βΌ (cardβπ΅))) |
22 | | domen2 9067 |
. . . . . 6
β’
((cardβπ΅)
β π΅ β (π΄ βΌ (cardβπ΅) β π΄ βΌ π΅)) |
23 | 21, 22 | sylan9bb 511 |
. . . . 5
β’
(((cardβπ΄)
β π΄ β§
(cardβπ΅) β
π΅) β
((cardβπ΄) βΌ
(cardβπ΅) β π΄ βΌ π΅)) |
24 | 13, 20, 23 | syl2anc 585 |
. . . 4
β’ (((π΄ β dom card β§ π΅ β π) β§ ((cardβπ΄) β β
β§ (cardβπ΄) β (cardβπ΅))) β ((cardβπ΄) βΌ (cardβπ΅) β π΄ βΌ π΅)) |
25 | 11, 24 | mpbid 231 |
. . 3
β’ (((π΄ β dom card β§ π΅ β π) β§ ((cardβπ΄) β β
β§ (cardβπ΄) β (cardβπ΅))) β π΄ βΌ π΅) |
26 | 25 | expr 458 |
. 2
β’ (((π΄ β dom card β§ π΅ β π) β§ (cardβπ΄) β β
) β ((cardβπ΄) β (cardβπ΅) β π΄ βΌ π΅)) |
27 | 7, 26 | pm2.61dane 3029 |
1
β’ ((π΄ β dom card β§ π΅ β π) β ((cardβπ΄) β (cardβπ΅) β π΄ βΌ π΅)) |