Theorem funcocnv2

Description: Precomposition with the converse. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by BJ, 25-Oct-2026)

	Ref	Expression
Assertion	funcocnv2	⊢ ( Fun 𝐹 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ran 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		df-fun	⊢ ( Fun 𝐹 ↔ ( Rel 𝐹 ∧ ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ) )
2	1	simprbi	⊢ ( Fun 𝐹 → ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I )
3		iss	⊢ ( ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ↔ ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ dom ( 𝐹 ∘ ◡ 𝐹 ) ) )
4	2 3	sylib	⊢ ( Fun 𝐹 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ dom ( 𝐹 ∘ ◡ 𝐹 ) ) )
5		dmcocnv2	⊢ dom ( 𝐹 ∘ ◡ 𝐹 ) = ran 𝐹
6	5	reseq2i	⊢ ( I ↾ dom ( 𝐹 ∘ ◡ 𝐹 ) ) = ( I ↾ ran 𝐹 )
7	4 6	eqtrdi	⊢ ( Fun 𝐹 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ran 𝐹 ) )