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 ( A o. B )

Proof

Step Hyp Ref Expression
1 df-co 
 |-  ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }
2 1 relopabiv 
 |-  Rel ( A o. B )