Step | Hyp | Ref
| Expression |
1 | | ficardom 9902 |
. . 3
β’ (π΅ β Fin β
(cardβπ΅) β
Ο) |
2 | | isinf 9207 |
. . 3
β’ (Β¬
π΄ β Fin β
βπ β Ο
βπ(π β π΄ β§ π β π)) |
3 | | breq2 5110 |
. . . . . 6
β’ (π = (cardβπ΅) β (π β π β π β (cardβπ΅))) |
4 | 3 | anbi2d 630 |
. . . . 5
β’ (π = (cardβπ΅) β ((π β π΄ β§ π β π) β (π β π΄ β§ π β (cardβπ΅)))) |
5 | 4 | exbidv 1925 |
. . . 4
β’ (π = (cardβπ΅) β (βπ(π β π΄ β§ π β π) β βπ(π β π΄ β§ π β (cardβπ΅)))) |
6 | 5 | rspcva 3578 |
. . 3
β’
(((cardβπ΅)
β Ο β§ βπ β Ο βπ(π β π΄ β§ π β π)) β βπ(π β π΄ β§ π β (cardβπ΅))) |
7 | 1, 2, 6 | syl2anr 598 |
. 2
β’ ((Β¬
π΄ β Fin β§ π΅ β Fin) β βπ(π β π΄ β§ π β (cardβπ΅))) |
8 | | simprr 772 |
. . . . . 6
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β π β (cardβπ΅)) |
9 | | ficardid 9903 |
. . . . . . 7
β’ (π΅ β Fin β
(cardβπ΅) β
π΅) |
10 | 9 | ad2antlr 726 |
. . . . . 6
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β (cardβπ΅) β π΅) |
11 | | entr 8949 |
. . . . . 6
β’ ((π β (cardβπ΅) β§ (cardβπ΅) β π΅) β π β π΅) |
12 | 8, 10, 11 | syl2anc 585 |
. . . . 5
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β π β π΅) |
13 | 12 | ensymd 8948 |
. . . 4
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β π΅ β π) |
14 | | bren 8896 |
. . . 4
β’ (π΅ β π β βπ π:π΅β1-1-ontoβπ) |
15 | 13, 14 | sylib 217 |
. . 3
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β βπ π:π΅β1-1-ontoβπ) |
16 | | f1of1 6784 |
. . . . . 6
β’ (π:π΅β1-1-ontoβπ β π:π΅β1-1βπ) |
17 | | simplrl 776 |
. . . . . 6
β’ ((((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β§ π:π΅β1-1-ontoβπ) β π β π΄) |
18 | | f1ss 6745 |
. . . . . 6
β’ ((π:π΅β1-1βπ β§ π β π΄) β π:π΅β1-1βπ΄) |
19 | 16, 17, 18 | syl2an2 685 |
. . . . 5
β’ ((((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β§ π:π΅β1-1-ontoβπ) β π:π΅β1-1βπ΄) |
20 | 19 | ex 414 |
. . . 4
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β (π:π΅β1-1-ontoβπ β π:π΅β1-1βπ΄)) |
21 | 20 | eximdv 1921 |
. . 3
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β (βπ π:π΅β1-1-ontoβπ β βπ π:π΅β1-1βπ΄)) |
22 | 15, 21 | mpd 15 |
. 2
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β βπ π:π΅β1-1βπ΄) |
23 | 7, 22 | exlimddv 1939 |
1
β’ ((Β¬
π΄ β Fin β§ π΅ β Fin) β βπ π:π΅β1-1βπ΄) |