This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 ) )