Step | Hyp | Ref
| Expression |
1 | | isfi 8797 |
. . 3
β’ (π΄ β Fin β βπ₯ β Ο π΄ β π₯) |
2 | | carden 10353 |
. . . . 5
β’ ((π΄ β π β§ π₯ β Ο) β ((cardβπ΄) = (cardβπ₯) β π΄ β π₯)) |
3 | | cardnn 9765 |
. . . . . . . 8
β’ (π₯ β Ο β
(cardβπ₯) = π₯) |
4 | | eqtr 2759 |
. . . . . . . . 9
β’
(((cardβπ΄) =
(cardβπ₯) β§
(cardβπ₯) = π₯) β (cardβπ΄) = π₯) |
5 | 4 | expcom 415 |
. . . . . . . 8
β’
((cardβπ₯) =
π₯ β ((cardβπ΄) = (cardβπ₯) β (cardβπ΄) = π₯)) |
6 | 3, 5 | syl 17 |
. . . . . . 7
β’ (π₯ β Ο β
((cardβπ΄) =
(cardβπ₯) β
(cardβπ΄) = π₯)) |
7 | | eleq1a 2832 |
. . . . . . 7
β’ (π₯ β Ο β
((cardβπ΄) = π₯ β (cardβπ΄) β
Ο)) |
8 | 6, 7 | syld 47 |
. . . . . 6
β’ (π₯ β Ο β
((cardβπ΄) =
(cardβπ₯) β
(cardβπ΄) β
Ο)) |
9 | 8 | adantl 483 |
. . . . 5
β’ ((π΄ β π β§ π₯ β Ο) β ((cardβπ΄) = (cardβπ₯) β (cardβπ΄) β
Ο)) |
10 | 2, 9 | sylbird 260 |
. . . 4
β’ ((π΄ β π β§ π₯ β Ο) β (π΄ β π₯ β (cardβπ΄) β Ο)) |
11 | 10 | rexlimdva 3149 |
. . 3
β’ (π΄ β π β (βπ₯ β Ο π΄ β π₯ β (cardβπ΄) β Ο)) |
12 | 1, 11 | biimtrid 241 |
. 2
β’ (π΄ β π β (π΄ β Fin β (cardβπ΄) β
Ο)) |
13 | | cardnn 9765 |
. . . . . . . 8
β’
((cardβπ΄)
β Ο β (cardβ(cardβπ΄)) = (cardβπ΄)) |
14 | 13 | eqcomd 2742 |
. . . . . . 7
β’
((cardβπ΄)
β Ο β (cardβπ΄) = (cardβ(cardβπ΄))) |
15 | 14 | adantl 483 |
. . . . . 6
β’ ((π΄ β π β§ (cardβπ΄) β Ο) β (cardβπ΄) =
(cardβ(cardβπ΄))) |
16 | | carden 10353 |
. . . . . 6
β’ ((π΄ β π β§ (cardβπ΄) β Ο) β ((cardβπ΄) =
(cardβ(cardβπ΄))
β π΄ β
(cardβπ΄))) |
17 | 15, 16 | mpbid 231 |
. . . . 5
β’ ((π΄ β π β§ (cardβπ΄) β Ο) β π΄ β (cardβπ΄)) |
18 | 17 | ex 414 |
. . . 4
β’ (π΄ β π β ((cardβπ΄) β Ο β π΄ β (cardβπ΄))) |
19 | 18 | ancld 552 |
. . 3
β’ (π΄ β π β ((cardβπ΄) β Ο β ((cardβπ΄) β Ο β§ π΄ β (cardβπ΄)))) |
20 | | breq2 5085 |
. . . . 5
β’ (π₯ = (cardβπ΄) β (π΄ β π₯ β π΄ β (cardβπ΄))) |
21 | 20 | rspcev 3566 |
. . . 4
β’
(((cardβπ΄)
β Ο β§ π΄
β (cardβπ΄))
β βπ₯ β
Ο π΄ β π₯) |
22 | 21, 1 | sylibr 233 |
. . 3
β’
(((cardβπ΄)
β Ο β§ π΄
β (cardβπ΄))
β π΄ β
Fin) |
23 | 19, 22 | syl6 35 |
. 2
β’ (π΄ β π β ((cardβπ΄) β Ο β π΄ β Fin)) |
24 | 12, 23 | impbid 211 |
1
β’ (π΄ β π β (π΄ β Fin β (cardβπ΄) β
Ο)) |