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

Metamath Proof Explorer

Theorem coi1

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

Proof

Step Hyp Ref Expression
1 relco ⊢ Rel ( 𝐴 ∘ I )
2 vex ⊢ 𝑥 ∈ V
3 vex ⊢ 𝑦 ∈ V
4 2 3 opelco ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ I ) ↔ ∃ 𝑧 ( 𝑥 I 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
5 vex ⊢ 𝑧 ∈ V
6 5 ideq ⊢ ( 𝑥 I 𝑧 ↔ 𝑥 = 𝑧 )
7 equcom ⊢ ( 𝑥 = 𝑧 ↔ 𝑧 = 𝑥 )
8 6 7 bitri ⊢ ( 𝑥 I 𝑧 ↔ 𝑧 = 𝑥 )
9 8 anbi1i ⊢ ( ( 𝑥 I 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ( 𝑧 = 𝑥 ∧ 𝑧 𝐴 𝑦 ) )
10 9 exbii ⊢ ( ∃ 𝑧 ( 𝑥 I 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑧 𝐴 𝑦 ) )
11 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝐴 𝑦 ↔ 𝑥 𝐴 𝑦 ) )
12 11 equsexvw ⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑧 𝐴 𝑦 ) ↔ 𝑥 𝐴 𝑦 )
13 10 12 bitri ⊢ ( ∃ 𝑧 ( 𝑥 I 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ 𝑥 𝐴 𝑦 )
14 4 13 bitri ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ I ) ↔ 𝑥 𝐴 𝑦 )
15 df-br ⊢ ( 𝑥 𝐴 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
16 14 15 bitri ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 ∘ I ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 )
17 16 eqrelriv ⊢ ( ( Rel ( 𝐴 ∘ I ) ∧ Rel 𝐴 ) → ( 𝐴 ∘ I ) = 𝐴 )
18 1 17 mpan ⊢ ( Rel 𝐴 → ( 𝐴 ∘ I ) = 𝐴 )