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

Metamath Proof Explorer

Theorem relco

Description: A composition is a relation. Exercise 24 of TakeutiZaring p. 25. (Contributed by NM, 26-Jan-1997)

Ref Expression
Assertion relco Rel ( 𝐴 ∘ 𝐵 )

Proof

Step Hyp Ref Expression
1 df-co ⊢ ( 𝐴 ∘ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( 𝑥 𝐵 𝑧 ∧ 𝑧 𝐴 𝑦 ) }
2 1 relopabiv ⊢ Rel ( 𝐴 ∘ 𝐵 )