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 ◡ 𝐹 → ◡ ( 𝐹 ↾ 𝐴 ) = ( ◡ 𝐹 ↾ ( 𝐹 “ 𝐴 ) ) )