Theorem f1cocnv2

Description: Composition of an injective function with its converse. (Contributed by FL, 11-Nov-2011)

	Ref	Expression
Assertion	f1cocnv2	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ran 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		f1fun	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → Fun 𝐹 )
2		funcocnv2	⊢ ( Fun 𝐹 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ran 𝐹 ) )
3	1 2	syl	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ran 𝐹 ) )