Metamath Proof Explorer


Theorem f1orescnv

Description: The converse of a one-to-one-onto restricted function. (Contributed by Paul Chapman, 21-Apr-2008)

Ref Expression
Assertion f1orescnv ( ( Fun 𝐹 ∧ ( 𝐹𝑅 ) : 𝑅1-1-onto𝑃 ) → ( 𝐹𝑃 ) : 𝑃1-1-onto𝑅 )

Proof

Step Hyp Ref Expression
1 f1ocnv ( ( 𝐹𝑅 ) : 𝑅1-1-onto𝑃 ( 𝐹𝑅 ) : 𝑃1-1-onto𝑅 )
2 1 adantl ( ( Fun 𝐹 ∧ ( 𝐹𝑅 ) : 𝑅1-1-onto𝑃 ) → ( 𝐹𝑅 ) : 𝑃1-1-onto𝑅 )
3 funcnvres ( Fun 𝐹 ( 𝐹𝑅 ) = ( 𝐹 ↾ ( 𝐹𝑅 ) ) )
4 df-ima ( 𝐹𝑅 ) = ran ( 𝐹𝑅 )
5 dff1o5 ( ( 𝐹𝑅 ) : 𝑅1-1-onto𝑃 ↔ ( ( 𝐹𝑅 ) : 𝑅1-1𝑃 ∧ ran ( 𝐹𝑅 ) = 𝑃 ) )
6 5 simprbi ( ( 𝐹𝑅 ) : 𝑅1-1-onto𝑃 → ran ( 𝐹𝑅 ) = 𝑃 )
7 4 6 eqtrid ( ( 𝐹𝑅 ) : 𝑅1-1-onto𝑃 → ( 𝐹𝑅 ) = 𝑃 )
8 7 reseq2d ( ( 𝐹𝑅 ) : 𝑅1-1-onto𝑃 → ( 𝐹 ↾ ( 𝐹𝑅 ) ) = ( 𝐹𝑃 ) )
9 3 8 sylan9eq ( ( Fun 𝐹 ∧ ( 𝐹𝑅 ) : 𝑅1-1-onto𝑃 ) → ( 𝐹𝑅 ) = ( 𝐹𝑃 ) )
10 9 f1oeq1d ( ( Fun 𝐹 ∧ ( 𝐹𝑅 ) : 𝑅1-1-onto𝑃 ) → ( ( 𝐹𝑅 ) : 𝑃1-1-onto𝑅 ↔ ( 𝐹𝑃 ) : 𝑃1-1-onto𝑅 ) )
11 2 10 mpbid ( ( Fun 𝐹 ∧ ( 𝐹𝑅 ) : 𝑅1-1-onto𝑃 ) → ( 𝐹𝑃 ) : 𝑃1-1-onto𝑅 )