Step | Hyp | Ref
| Expression |
1 | | fnfun 6646 |
. . . . . 6
β’ (πΉ Fn π΄ β Fun πΉ) |
2 | | fdmrn 6746 |
. . . . . 6
β’ (Fun
πΉ β πΉ:dom πΉβΆran πΉ) |
3 | 1, 2 | sylib 217 |
. . . . 5
β’ (πΉ Fn π΄ β πΉ:dom πΉβΆran πΉ) |
4 | 3 | adantr 481 |
. . . 4
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β πΉ:dom πΉβΆran πΉ) |
5 | | fndm 6649 |
. . . . . 6
β’ (πΉ Fn π΄ β dom πΉ = π΄) |
6 | 5 | adantr 481 |
. . . . 5
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β dom πΉ = π΄) |
7 | | df-rn 5686 |
. . . . . . 7
β’ ran πΉ = dom β‘πΉ |
8 | | dmeq 5901 |
. . . . . . 7
β’ (β‘πΉ = πΉ β dom β‘πΉ = dom πΉ) |
9 | 7, 8 | eqtrid 2784 |
. . . . . 6
β’ (β‘πΉ = πΉ β ran πΉ = dom πΉ) |
10 | 9, 5 | sylan9eqr 2794 |
. . . . 5
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β ran πΉ = π΄) |
11 | 6, 10 | feq23d 6709 |
. . . 4
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β (πΉ:dom πΉβΆran πΉ β πΉ:π΄βΆπ΄)) |
12 | 4, 11 | mpbid 231 |
. . 3
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β πΉ:π΄βΆπ΄) |
13 | 1 | adantr 481 |
. . . 4
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β Fun πΉ) |
14 | | funeq 6565 |
. . . . 5
β’ (β‘πΉ = πΉ β (Fun β‘πΉ β Fun πΉ)) |
15 | 14 | adantl 482 |
. . . 4
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β (Fun β‘πΉ β Fun πΉ)) |
16 | 13, 15 | mpbird 256 |
. . 3
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β Fun β‘πΉ) |
17 | | df-f1 6545 |
. . 3
β’ (πΉ:π΄β1-1βπ΄ β (πΉ:π΄βΆπ΄ β§ Fun β‘πΉ)) |
18 | 12, 16, 17 | sylanbrc 583 |
. 2
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β πΉ:π΄β1-1βπ΄) |
19 | | simpl 483 |
. . 3
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β πΉ Fn π΄) |
20 | | df-fo 6546 |
. . 3
β’ (πΉ:π΄βontoβπ΄ β (πΉ Fn π΄ β§ ran πΉ = π΄)) |
21 | 19, 10, 20 | sylanbrc 583 |
. 2
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β πΉ:π΄βontoβπ΄) |
22 | | df-f1o 6547 |
. 2
β’ (πΉ:π΄β1-1-ontoβπ΄ β (πΉ:π΄β1-1βπ΄ β§ πΉ:π΄βontoβπ΄)) |
23 | 18, 21, 22 | sylanbrc 583 |
1
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β πΉ:π΄β1-1-ontoβπ΄) |