Step | Hyp | Ref
| Expression |
1 | | cardid2 9896 |
. . . . . . . 8
β’ (π΄ β dom card β
(cardβπ΄) β
π΄) |
2 | 1 | ensymd 8952 |
. . . . . . 7
β’ (π΄ β dom card β π΄ β (cardβπ΄)) |
3 | | entr 8953 |
. . . . . . . 8
β’ ((π¦ β π΄ β§ π΄ β (cardβπ΄)) β π¦ β (cardβπ΄)) |
4 | 3 | expcom 415 |
. . . . . . 7
β’ (π΄ β (cardβπ΄) β (π¦ β π΄ β π¦ β (cardβπ΄))) |
5 | 2, 4 | syl 17 |
. . . . . 6
β’ (π΄ β dom card β (π¦ β π΄ β π¦ β (cardβπ΄))) |
6 | | entr 8953 |
. . . . . . . 8
β’ ((π¦ β (cardβπ΄) β§ (cardβπ΄) β π΄) β π¦ β π΄) |
7 | 6 | expcom 415 |
. . . . . . 7
β’
((cardβπ΄)
β π΄ β (π¦ β (cardβπ΄) β π¦ β π΄)) |
8 | 1, 7 | syl 17 |
. . . . . 6
β’ (π΄ β dom card β (π¦ β (cardβπ΄) β π¦ β π΄)) |
9 | 5, 8 | impbid 211 |
. . . . 5
β’ (π΄ β dom card β (π¦ β π΄ β π¦ β (cardβπ΄))) |
10 | 9 | rabbidv 3418 |
. . . 4
β’ (π΄ β dom card β {π¦ β On β£ π¦ β π΄} = {π¦ β On β£ π¦ β (cardβπ΄)}) |
11 | 10 | inteqd 4917 |
. . 3
β’ (π΄ β dom card β β© {π¦
β On β£ π¦ β
π΄} = β© {π¦
β On β£ π¦ β
(cardβπ΄)}) |
12 | | cardval3 9895 |
. . 3
β’ (π΄ β dom card β
(cardβπ΄) = β© {π¦
β On β£ π¦ β
π΄}) |
13 | | cardon 9887 |
. . . 4
β’
(cardβπ΄)
β On |
14 | | oncardval 9898 |
. . . 4
β’
((cardβπ΄)
β On β (cardβ(cardβπ΄)) = β© {π¦ β On β£ π¦ β (cardβπ΄)}) |
15 | 13, 14 | mp1i 13 |
. . 3
β’ (π΄ β dom card β
(cardβ(cardβπ΄))
= β© {π¦ β On β£ π¦ β (cardβπ΄)}) |
16 | 11, 12, 15 | 3eqtr4rd 2788 |
. 2
β’ (π΄ β dom card β
(cardβ(cardβπ΄))
= (cardβπ΄)) |
17 | | card0 9901 |
. . 3
β’
(cardββ
) = β
|
18 | | ndmfv 6882 |
. . . 4
β’ (Β¬
π΄ β dom card β
(cardβπ΄) =
β
) |
19 | 18 | fveq2d 6851 |
. . 3
β’ (Β¬
π΄ β dom card β
(cardβ(cardβπ΄))
= (cardββ
)) |
20 | 17, 19, 18 | 3eqtr4a 2803 |
. 2
β’ (Β¬
π΄ β dom card β
(cardβ(cardβπ΄))
= (cardβπ΄)) |
21 | 16, 20 | pm2.61i 182 |
1
β’
(cardβ(cardβπ΄)) = (cardβπ΄) |