Theorem funcocnv2

Description: Composition with the converse. (Contributed by Jeff Madsen, 2-Sep-2009)

	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		dfdm4	⊢ dom 𝐹 = ran ◡ 𝐹
5		dmcoeq	⊢ ( dom 𝐹 = ran ◡ 𝐹 → dom ( 𝐹 ∘ ◡ 𝐹 ) = dom ◡ 𝐹 )
6	4 5	ax-mp	⊢ dom ( 𝐹 ∘ ◡ 𝐹 ) = dom ◡ 𝐹
7		df-rn	⊢ ran 𝐹 = dom ◡ 𝐹
8	6 7	eqtr4i	⊢ dom ( 𝐹 ∘ ◡ 𝐹 ) = ran 𝐹
9	8	reseq2i	⊢ ( I ↾ dom ( 𝐹 ∘ ◡ 𝐹 ) ) = ( I ↾ ran 𝐹 )
10	9	eqeq2i	⊢ ( ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ dom ( 𝐹 ∘ ◡ 𝐹 ) ) ↔ ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ran 𝐹 ) )
11	3 10	bitri	⊢ ( ( 𝐹 ∘ ◡ 𝐹 ) ⊆ I ↔ ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ran 𝐹 ) )
12	2 11	sylib	⊢ ( Fun 𝐹 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ ran 𝐹 ) )