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 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β π΅ β Fin) |
11 | | relen 8895 |
. . . . . . . . . . . . . . 15
β’ Rel
β |
12 | 11 | brrelex1i 5693 |
. . . . . . . . . . . . . 14
β’ (π΄ β π΅ β π΄ β V) |
13 | 5, 12 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β π΄ β V) |
14 | 10, 13 | elmapd 8786 |
. . . . . . . . . . . 12
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β (πΉ β (π΅ βm π΄) β πΉ:π΄βΆπ΅)) |
15 | 3, 14 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β πΉ β (π΅ βm π΄)) |
16 | | f1f1orn 6800 |
. . . . . . . . . . . 12
β’ (πΉ:π΄β1-1βπ΅ β πΉ:π΄β1-1-ontoβran
πΉ) |
17 | 16 | adantl 483 |
. . . . . . . . . . 11
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β πΉ:π΄β1-1-ontoβran
πΉ) |
18 | | f1oen3g 8913 |
. . . . . . . . . . 11
β’ ((πΉ β (π΅ βm π΄) β§ πΉ:π΄β1-1-ontoβran
πΉ) β π΄ β ran πΉ) |
19 | 15, 17, 18 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β π΄ β ran πΉ) |
20 | | php3 9163 |
. . . . . . . . . . . 12
β’ ((π΅ β Fin β§ ran πΉ β π΅) β ran πΉ βΊ π΅) |
21 | 20 | ex 414 |
. . . . . . . . . . 11
β’ (π΅ β Fin β (ran πΉ β π΅ β ran πΉ βΊ π΅)) |
22 | 10, 21 | syl 17 |
. . . . . . . . . 10
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β (ran πΉ β π΅ β ran πΉ βΊ π΅)) |
23 | | ensdomtr 9064 |
. . . . . . . . . 10
β’ ((π΄ β ran πΉ β§ ran πΉ βΊ π΅) β π΄ βΊ π΅) |
24 | 19, 22, 23 | syl6an 683 |
. . . . . . . . 9
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β (ran πΉ β π΅ β π΄ βΊ π΅)) |
25 | | sdomnen 8928 |
. . . . . . . . 9
β’ (π΄ βΊ π΅ β Β¬ π΄ β π΅) |
26 | 24, 25 | syl6 35 |
. . . . . . . 8
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β (ran πΉ β π΅ β Β¬ π΄ β π΅)) |
27 | 9, 26 | sylbird 260 |
. . . . . . 7
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β (ran πΉ β π΅ β Β¬ π΄ β π΅)) |
28 | 27 | necon4ad 2963 |
. . . . . 6
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β (π΄ β π΅ β ran πΉ = π΅)) |
29 | 5, 28 | mpd 15 |
. . . . 5
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β ran πΉ = π΅) |
30 | | df-fo 6507 |
. . . . 5
β’ (πΉ:π΄βontoβπ΅ β (πΉ Fn π΄ β§ ran πΉ = π΅)) |
31 | 4, 29, 30 | sylanbrc 584 |
. . . 4
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β πΉ:π΄βontoβπ΅) |
32 | | df-f1o 6508 |
. . . 4
β’ (πΉ:π΄β1-1-ontoβπ΅ β (πΉ:π΄β1-1βπ΅ β§ πΉ:π΄βontoβπ΅)) |
33 | 1, 31, 32 | sylanbrc 584 |
. . 3
β’ (((π΄ β π΅ β§ π΅ β Fin) β§ πΉ:π΄β1-1βπ΅) β πΉ:π΄β1-1-ontoβπ΅) |
34 | 33 | ex 414 |
. 2
β’ ((π΄ β π΅ β§ π΅ β Fin) β (πΉ:π΄β1-1βπ΅ β πΉ:π΄β1-1-ontoβπ΅)) |
35 | | f1of1 6788 |
. 2
β’ (πΉ:π΄β1-1-ontoβπ΅ β πΉ:π΄β1-1βπ΅) |
36 | 34, 35 | impbid1 224 |
1
β’ ((π΄ β π΅ β§ π΅ β Fin) β (πΉ:π΄β1-1βπ΅ β πΉ:π΄β1-1-ontoβπ΅)) |