Step | Hyp | Ref
| Expression |
1 | | fnfun 6650 |
. . . . . 6
β’ (πΉ Fn π΄ β Fun πΉ) |
2 | | fdmrn 6750 |
. . . . . 6
β’ (Fun
πΉ β πΉ:dom πΉβΆran πΉ) |
3 | 1, 2 | sylib 217 |
. . . . 5
β’ (πΉ Fn π΄ β πΉ:dom πΉβΆran πΉ) |
4 | 3 | adantr 482 |
. . . 4
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β πΉ:dom πΉβΆran πΉ) |
5 | | fndm 6653 |
. . . . . 6
β’ (πΉ Fn π΄ β dom πΉ = π΄) |
6 | 5 | adantr 482 |
. . . . 5
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β dom πΉ = π΄) |
7 | | df-rn 5688 |
. . . . . . 7
β’ ran πΉ = dom β‘πΉ |
8 | | dmeq 5904 |
. . . . . . 7
β’ (β‘πΉ = πΉ β dom β‘πΉ = dom πΉ) |
9 | 7, 8 | eqtrid 2785 |
. . . . . 6
β’ (β‘πΉ = πΉ β ran πΉ = dom πΉ) |
10 | 9, 5 | sylan9eqr 2795 |
. . . . 5
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β ran πΉ = π΄) |
11 | 6, 10 | feq23d 6713 |
. . . 4
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β (πΉ:dom πΉβΆran πΉ β πΉ:π΄βΆπ΄)) |
12 | 4, 11 | mpbid 231 |
. . 3
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β πΉ:π΄βΆπ΄) |
13 | 1 | adantr 482 |
. . . 4
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β Fun πΉ) |
14 | | funeq 6569 |
. . . . 5
β’ (β‘πΉ = πΉ β (Fun β‘πΉ β Fun πΉ)) |
15 | 14 | adantl 483 |
. . . 4
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β (Fun β‘πΉ β Fun πΉ)) |
16 | 13, 15 | mpbird 257 |
. . 3
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β Fun β‘πΉ) |
17 | | df-f1 6549 |
. . 3
β’ (πΉ:π΄β1-1βπ΄ β (πΉ:π΄βΆπ΄ β§ Fun β‘πΉ)) |
18 | 12, 16, 17 | sylanbrc 584 |
. 2
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β πΉ:π΄β1-1βπ΄) |
19 | | simpl 484 |
. . 3
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β πΉ Fn π΄) |
20 | | df-fo 6550 |
. . 3
β’ (πΉ:π΄βontoβπ΄ β (πΉ Fn π΄ β§ ran πΉ = π΄)) |
21 | 19, 10, 20 | sylanbrc 584 |
. 2
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β πΉ:π΄βontoβπ΄) |
22 | | df-f1o 6551 |
. 2
β’ (πΉ:π΄β1-1-ontoβπ΄ β (πΉ:π΄β1-1βπ΄ β§ πΉ:π΄βontoβπ΄)) |
23 | 18, 21, 22 | sylanbrc 584 |
1
β’ ((πΉ Fn π΄ β§ β‘πΉ = πΉ) β πΉ:π΄β1-1-ontoβπ΄) |