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 ⁡ F → F ∘ F -1 = I ↾ ran ⁡ F

Proof

Step Hyp Ref Expression
1 df-fun ⊢ Fun ⁡ F ↔ Rel ⁡ F ∧ F ∘ F -1 ⊆ I
2 1 simprbi ⊢ Fun ⁡ F → F ∘ F -1 ⊆ I
3 iss ⊢ F ∘ F -1 ⊆ I ↔ F ∘ F -1 = I ↾ dom ⁡ F ∘ F -1
4 dfdm4 ⊢ dom ⁡ F = ran ⁡ F -1
5 dmcoeq ⊢ dom ⁡ F = ran ⁡ F -1 → dom ⁡ F ∘ F -1 = dom ⁡ F -1
6 4 5 ax-mp ⊢ dom ⁡ F ∘ F -1 = dom ⁡ F -1
7 df-rn ⊢ ran ⁡ F = dom ⁡ F -1
8 6 7 eqtr4i ⊢ dom ⁡ F ∘ F -1 = ran ⁡ F
9 8 reseq2i ⊢ I ↾ dom ⁡ F ∘ F -1 = I ↾ ran ⁡ F
10 9 eqeq2i ⊢ F ∘ F -1 = I ↾ dom ⁡ F ∘ F -1 ↔ F ∘ F -1 = I ↾ ran ⁡ F
11 3 10 bitri ⊢ F ∘ F -1 ⊆ I ↔ F ∘ F -1 = I ↾ ran ⁡ F
12 2 11 sylib ⊢ Fun ⁡ F → F ∘ F -1 = I ↾ ran ⁡ F