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 ) = 𝐴 )