Theorem fococnv2

Description: The composition of an onto function and its converse. (Contributed by Stefan O'Rear, 12-Feb-2015)

	Ref	Expression
Assertion	fococnv2	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fofun	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → Fun 𝐹 )
2		funcocnv2	⊢ ( Fun 𝐹 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ran 𝐹 ) )
3	1 2	syl	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ran 𝐹 ) )
4		forn	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
5	4	reseq2d	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( I ↾ ran 𝐹 ) = ( I ↾ 𝐵 ) )
6	3 5	eqtrd	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ 𝐵 ) )