Step |
Hyp |
Ref |
Expression |
1 |
|
tposfn2 |
|- ( Rel A -> ( F Fn A -> tpos F Fn `' A ) ) |
2 |
1
|
adantrd |
|- ( Rel A -> ( ( F Fn A /\ ran F = B ) -> tpos F Fn `' A ) ) |
3 |
|
fndm |
|- ( F Fn A -> dom F = A ) |
4 |
3
|
releqd |
|- ( F Fn A -> ( Rel dom F <-> Rel A ) ) |
5 |
4
|
biimparc |
|- ( ( Rel A /\ F Fn A ) -> Rel dom F ) |
6 |
|
rntpos |
|- ( Rel dom F -> ran tpos F = ran F ) |
7 |
5 6
|
syl |
|- ( ( Rel A /\ F Fn A ) -> ran tpos F = ran F ) |
8 |
7
|
eqeq1d |
|- ( ( Rel A /\ F Fn A ) -> ( ran tpos F = B <-> ran F = B ) ) |
9 |
8
|
biimprd |
|- ( ( Rel A /\ F Fn A ) -> ( ran F = B -> ran tpos F = B ) ) |
10 |
9
|
expimpd |
|- ( Rel A -> ( ( F Fn A /\ ran F = B ) -> ran tpos F = B ) ) |
11 |
2 10
|
jcad |
|- ( Rel A -> ( ( F Fn A /\ ran F = B ) -> ( tpos F Fn `' A /\ ran tpos F = B ) ) ) |
12 |
|
df-fo |
|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) ) |
13 |
|
df-fo |
|- ( tpos F : `' A -onto-> B <-> ( tpos F Fn `' A /\ ran tpos F = B ) ) |
14 |
11 12 13
|
3imtr4g |
|- ( Rel A -> ( F : A -onto-> B -> tpos F : `' A -onto-> B ) ) |