Step |
Hyp |
Ref |
Expression |
1 |
|
f1ocnv |
|- ( ( F |` R ) : R -1-1-onto-> P -> `' ( F |` R ) : P -1-1-onto-> R ) |
2 |
1
|
adantl |
|- ( ( Fun `' F /\ ( F |` R ) : R -1-1-onto-> P ) -> `' ( F |` R ) : P -1-1-onto-> R ) |
3 |
|
funcnvres |
|- ( Fun `' F -> `' ( F |` R ) = ( `' F |` ( F " R ) ) ) |
4 |
|
df-ima |
|- ( F " R ) = ran ( F |` R ) |
5 |
|
dff1o5 |
|- ( ( F |` R ) : R -1-1-onto-> P <-> ( ( F |` R ) : R -1-1-> P /\ ran ( F |` R ) = P ) ) |
6 |
5
|
simprbi |
|- ( ( F |` R ) : R -1-1-onto-> P -> ran ( F |` R ) = P ) |
7 |
4 6
|
eqtrid |
|- ( ( F |` R ) : R -1-1-onto-> P -> ( F " R ) = P ) |
8 |
7
|
reseq2d |
|- ( ( F |` R ) : R -1-1-onto-> P -> ( `' F |` ( F " R ) ) = ( `' F |` P ) ) |
9 |
3 8
|
sylan9eq |
|- ( ( Fun `' F /\ ( F |` R ) : R -1-1-onto-> P ) -> `' ( F |` R ) = ( `' F |` P ) ) |
10 |
9
|
f1oeq1d |
|- ( ( Fun `' F /\ ( F |` R ) : R -1-1-onto-> P ) -> ( `' ( F |` R ) : P -1-1-onto-> R <-> ( `' F |` P ) : P -1-1-onto-> R ) ) |
11 |
2 10
|
mpbid |
|- ( ( Fun `' F /\ ( F |` R ) : R -1-1-onto-> P ) -> ( `' F |` P ) : P -1-1-onto-> R ) |