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 ⁡ A → A ∘ I = A

Proof

Step Hyp Ref Expression
1 relco ⊢ Rel ⁡ A ∘ I
2 vex ⊢ x ∈ V
3 vex ⊢ y ∈ V
4 2 3 opelco ⊢ x y ∈ A ∘ I ↔ ∃ z x I z ∧ z A y
5 vex ⊢ z ∈ V
6 5 ideq ⊢ x I z ↔ x = z
7 equcom ⊢ x = z ↔ z = x
8 6 7 bitri ⊢ x I z ↔ z = x
9 8 anbi1i ⊢ x I z ∧ z A y ↔ z = x ∧ z A y
10 9 exbii ⊢ ∃ z x I z ∧ z A y ↔ ∃ z z = x ∧ z A y
11 breq1 ⊢ z = x → z A y ↔ x A y
12 11 equsexvw ⊢ ∃ z z = x ∧ z A y ↔ x A y
13 10 12 bitri ⊢ ∃ z x I z ∧ z A y ↔ x A y
14 4 13 bitri ⊢ x y ∈ A ∘ I ↔ x A y
15 df-br ⊢ x A y ↔ x y ∈ A
16 14 15 bitri ⊢ x y ∈ A ∘ I ↔ x y ∈ A
17 16 eqrelriv ⊢ Rel ⁡ A ∘ I ∧ Rel ⁡ A → A ∘ I = A
18 1 17 mpan ⊢ Rel ⁡ A → A ∘ I = A