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

Metamath Proof Explorer

Theorem coi2

Description: Composition with the identity relation. Part of Theorem 3.7(i) of Monk1 p. 36. (Contributed by NM, 22-Apr-2004)

Ref Expression
Assertion coi2 ⊢ Rel ⁡ A → I ∘ A = A

Proof

Step Hyp Ref Expression
1 dfrel2 ⊢ Rel ⁡ A ↔ A -1 -1 = A
2 cnvco ⊢ A -1 ∘ I -1 = I -1 ∘ A -1 -1
3 relcnv ⊢ Rel ⁡ A -1
4 coi1 ⊢ Rel ⁡ A -1 → A -1 ∘ I = A -1
5 3 4 ax-mp ⊢ A -1 ∘ I = A -1
6 5 cnveqi ⊢ A -1 ∘ I -1 = A -1 -1
7 2 6 eqtr3i ⊢ I -1 ∘ A -1 -1 = A -1 -1
8 cnvi ⊢ I -1 = I
9 coeq2 ⊢ A -1 -1 = A → I -1 ∘ A -1 -1 = I -1 ∘ A
10 coeq1 ⊢ I -1 = I → I -1 ∘ A = I ∘ A
11 9 10 sylan9eq ⊢ A -1 -1 = A ∧ I -1 = I → I -1 ∘ A -1 -1 = I ∘ A
12 8 11 mpan2 ⊢ A -1 -1 = A → I -1 ∘ A -1 -1 = I ∘ A
13 id ⊢ A -1 -1 = A → A -1 -1 = A
14 7 12 13 3eqtr3a ⊢ A -1 -1 = A → I ∘ A = A
15 1 14 sylbi ⊢ Rel ⁡ A → I ∘ A = A