Step | Hyp | Ref
| Expression |
1 | | ficardom 9955 |
. . 3
β’ (π΅ β Fin β
(cardβπ΅) β
Ο) |
2 | | isinf 9259 |
. . 3
β’ (Β¬
π΄ β Fin β
βπ β Ο
βπ(π β π΄ β§ π β π)) |
3 | | breq2 5145 |
. . . . . 6
β’ (π = (cardβπ΅) β (π β π β π β (cardβπ΅))) |
4 | 3 | anbi2d 628 |
. . . . 5
β’ (π = (cardβπ΅) β ((π β π΄ β§ π β π) β (π β π΄ β§ π β (cardβπ΅)))) |
5 | 4 | exbidv 1916 |
. . . 4
β’ (π = (cardβπ΅) β (βπ(π β π΄ β§ π β π) β βπ(π β π΄ β§ π β (cardβπ΅)))) |
6 | 5 | rspcva 3604 |
. . 3
β’
(((cardβπ΅)
β Ο β§ βπ β Ο βπ(π β π΄ β§ π β π)) β βπ(π β π΄ β§ π β (cardβπ΅))) |
7 | 1, 2, 6 | syl2anr 596 |
. 2
β’ ((Β¬
π΄ β Fin β§ π΅ β Fin) β βπ(π β π΄ β§ π β (cardβπ΅))) |
8 | | simprr 770 |
. . . . . 6
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β π β (cardβπ΅)) |
9 | | ficardid 9956 |
. . . . . . 7
β’ (π΅ β Fin β
(cardβπ΅) β
π΅) |
10 | 9 | ad2antlr 724 |
. . . . . 6
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β (cardβπ΅) β π΅) |
11 | | entr 9001 |
. . . . . 6
β’ ((π β (cardβπ΅) β§ (cardβπ΅) β π΅) β π β π΅) |
12 | 8, 10, 11 | syl2anc 583 |
. . . . 5
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β π β π΅) |
13 | 12 | ensymd 9000 |
. . . 4
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β π΅ β π) |
14 | | bren 8948 |
. . . 4
β’ (π΅ β π β βπ π:π΅β1-1-ontoβπ) |
15 | 13, 14 | sylib 217 |
. . 3
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β βπ π:π΅β1-1-ontoβπ) |
16 | | f1of1 6825 |
. . . . . 6
β’ (π:π΅β1-1-ontoβπ β π:π΅β1-1βπ) |
17 | | simplrl 774 |
. . . . . 6
β’ ((((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β§ π:π΅β1-1-ontoβπ) β π β π΄) |
18 | | f1ss 6786 |
. . . . . 6
β’ ((π:π΅β1-1βπ β§ π β π΄) β π:π΅β1-1βπ΄) |
19 | 16, 17, 18 | syl2an2 683 |
. . . . 5
β’ ((((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β§ π:π΅β1-1-ontoβπ) β π:π΅β1-1βπ΄) |
20 | 19 | ex 412 |
. . . 4
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β (π:π΅β1-1-ontoβπ β π:π΅β1-1βπ΄)) |
21 | 20 | eximdv 1912 |
. . 3
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β (βπ π:π΅β1-1-ontoβπ β βπ π:π΅β1-1βπ΄)) |
22 | 15, 21 | mpd 15 |
. 2
β’ (((Β¬
π΄ β Fin β§ π΅ β Fin) β§ (π β π΄ β§ π β (cardβπ΅))) β βπ π:π΅β1-1βπ΄) |
23 | 7, 22 | exlimddv 1930 |
1
β’ ((Β¬
π΄ β Fin β§ π΅ β Fin) β βπ π:π΅β1-1βπ΄) |