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

Metamath Proof Explorer

Theorem funcnvres

Description: The converse of a restricted function. (Contributed by NM, 27-Mar-1998)

Ref Expression
Assertion funcnvres ( Fun ◡ 𝐹 → ◡ ( 𝐹 ↾ 𝐴 ) = ( ◡ 𝐹 ↾ ( 𝐹 “ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 df-ima ⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
2 df-rn ⊢ ran ( 𝐹 ↾ 𝐴 ) = dom ◡ ( 𝐹 ↾ 𝐴 )
3 1 2 eqtri ⊢ ( 𝐹 “ 𝐴 ) = dom ◡ ( 𝐹 ↾ 𝐴 )
4 3 reseq2i ⊢ ( ◡ 𝐹 ↾ ( 𝐹 “ 𝐴 ) ) = ( ◡ 𝐹 ↾ dom ◡ ( 𝐹 ↾ 𝐴 ) )
5 resss ⊢ ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹
6 cnvss ⊢ ( ( 𝐹 ↾ 𝐴 ) ⊆ 𝐹 → ◡ ( 𝐹 ↾ 𝐴 ) ⊆ ◡ 𝐹 )
7 5 6 ax-mp ⊢ ◡ ( 𝐹 ↾ 𝐴 ) ⊆ ◡ 𝐹
8 funssres ⊢ ( ( Fun ◡ 𝐹 ∧ ◡ ( 𝐹 ↾ 𝐴 ) ⊆ ◡ 𝐹 ) → ( ◡ 𝐹 ↾ dom ◡ ( 𝐹 ↾ 𝐴 ) ) = ◡ ( 𝐹 ↾ 𝐴 ) )
9 7 8 mpan2 ⊢ ( Fun ◡ 𝐹 → ( ◡ 𝐹 ↾ dom ◡ ( 𝐹 ↾ 𝐴 ) ) = ◡ ( 𝐹 ↾ 𝐴 ) )
10 4 9 eqtr2id ⊢ ( Fun ◡ 𝐹 → ◡ ( 𝐹 ↾ 𝐴 ) = ( ◡ 𝐹 ↾ ( 𝐹 “ 𝐴 ) ) )