Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . 4
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β πΉ:π΄β1-1βπ΅) |
2 | | f1f 6743 |
. . . . . . 7
β’ (πΉ:π΄β1-1βπ΅ β πΉ:π΄βΆπ΅) |
3 | 2 | adantl 483 |
. . . . . 6
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β πΉ:π΄βΆπ΅) |
4 | 3 | ffnd 6674 |
. . . . 5
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β πΉ Fn π΄) |
5 | | simpll 766 |
. . . . . 6
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β π΄ β π΅) |
6 | 3 | frnd 6681 |
. . . . . . . . 9
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β ran πΉ β π΅) |
7 | | df-pss 3934 |
. . . . . . . . . 10
β’ (ran
πΉ β π΅ β (ran πΉ β π΅ β§ ran πΉ β π΅)) |
8 | 7 | baib 537 |
. . . . . . . . 9
β’ (ran
πΉ β π΅ β (ran πΉ β π΅ β ran πΉ β π΅)) |
9 | 6, 8 | syl 17 |
. . . . . . . 8
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β (ran πΉ β π΅ β ran πΉ β π΅)) |
10 | | php3 9163 |
. . . . . . . . . . . 12
β’ ((π΅ β Fin β§ ran πΉ β π΅) β ran πΉ βΊ π΅) |
11 | 10 | ex 414 |
. . . . . . . . . . 11
β’ (π΅ β Fin β (ran πΉ β π΅ β ran πΉ βΊ π΅)) |
12 | 11 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β (ran πΉ β π΅ β ran πΉ βΊ π΅)) |
13 | | enfii 9140 |
. . . . . . . . . . . 12
β’ ((π΅ β Fin β§ π΄ β π΅) β π΄ β Fin) |
14 | 13 | ancoms 460 |
. . . . . . . . . . 11
β’ ((π΄ β π΅ β§ π΅ β Fin) β π΄ β Fin) |
15 | | f1f1orn 6800 |
. . . . . . . . . . . 12
β’ (πΉ:π΄β1-1βπ΅ β πΉ:π΄β1-1-ontoβran
πΉ) |
16 | | f1oenfi 9133 |
. . . . . . . . . . . 12
β’ ((π΄ β Fin β§ πΉ:π΄β1-1-ontoβran
πΉ) β π΄ β ran πΉ) |
17 | 14, 15, 16 | syl2an 597 |
. . . . . . . . . . 11
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β π΄ β ran πΉ) |
18 | | endom 8926 |
. . . . . . . . . . . . 13
β’ (π΄ β ran πΉ β π΄ βΌ ran πΉ) |
19 | | domsdomtrfi 9156 |
. . . . . . . . . . . . 13
β’ ((π΄ β Fin β§ π΄ βΌ ran πΉ β§ ran πΉ βΊ π΅) β π΄ βΊ π΅) |
20 | 18, 19 | syl3an2 1165 |
. . . . . . . . . . . 12
β’ ((π΄ β Fin β§ π΄ β ran πΉ β§ ran πΉ βΊ π΅) β π΄ βΊ π΅) |
21 | 20 | 3expia 1122 |
. . . . . . . . . . 11
β’ ((π΄ β Fin β§ π΄ β ran πΉ) β (ran πΉ βΊ π΅ β π΄ βΊ π΅)) |
22 | 14, 17, 21 | syl2an2r 684 |
. . . . . . . . . 10
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β (ran πΉ βΊ π΅ β π΄ βΊ π΅)) |
23 | 12, 22 | syld 47 |
. . . . . . . . 9
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β (ran πΉ β π΅ β π΄ βΊ π΅)) |
24 | | sdomnen 8928 |
. . . . . . . . 9
β’ (π΄ βΊ π΅ β Β¬ π΄ β π΅) |
25 | 23, 24 | syl6 35 |
. . . . . . . 8
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β (ran πΉ β π΅ β Β¬ π΄ β π΅)) |
26 | 9, 25 | sylbird 260 |
. . . . . . 7
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β (ran πΉ β π΅ β Β¬ π΄ β π΅)) |
27 | 26 | necon4ad 2963 |
. . . . . 6
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β (π΄ β π΅ β ran πΉ = π΅)) |
28 | 5, 27 | mpd 15 |
. . . . 5
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β ran πΉ = π΅) |
29 | | df-fo 6507 |
. . . . 5
β’ (πΉ:π΄βontoβπ΅ β (πΉ Fn π΄ β§ ran πΉ = π΅)) |
30 | 4, 28, 29 | sylanbrc 584 |
. . . 4
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β πΉ:π΄βontoβπ΅) |
31 | | df-f1o 6508 |
. . . 4
β’ (πΉ:π΄β1-1-ontoβπ΅ β (πΉ:π΄β1-1βπ΅ β§ πΉ:π΄βontoβπ΅)) |
32 | 1, 30, 31 | sylanbrc 584 |
. . 3
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β πΉ:π΄β1-1-ontoβπ΅) |
33 | 32 | ex 414 |
. 2
β’ ((π΄ β π΅ β§ π΅ β Fin) β (πΉ:π΄β1-1βπ΅ β πΉ:π΄β1-1-ontoβπ΅)) |
34 | | f1of1 6788 |
. 2
β’ (πΉ:π΄β1-1-ontoβπ΅ β πΉ:π΄β1-1βπ΅) |
35 | 33, 34 | impbid1 224 |
1
β’ ((π΄ β π΅ β§ π΅ β Fin) β (πΉ:π΄β1-1βπ΅ β πΉ:π΄β1-1-ontoβπ΅)) |