This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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→ 𝑅 )