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 𝐴 → ( I ∘ 𝐴 ) = 𝐴 )

Proof

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