Metamath Proof Explorer

Theorem cotrg

Description: Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr for the main application. (Contributed by NM, 27-Dec-1996) (Proof shortened by Andrew Salmon, 27-Aug-2011) Generalized from its special instance cotr . (Revised by Richard Penner, 24-Dec-2019)

Ref Expression
Assertion cotrg 
|- ( ( A o. B ) C_ C <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) )

Proof

Step Hyp Ref Expression
1 df-co 
 |-  ( A o. B ) = { <. x , z >. | E. y ( x B y /\ y A z ) }
2 1 relopabi 
 |-  Rel ( A o. B )
3 ssrel 
 |-  ( Rel ( A o. B ) -> ( ( A o. B ) C_ C <-> A. x A. z ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) ) )
4 2 3 ax-mp 
 |-  ( ( A o. B ) C_ C <-> A. x A. z ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) )
5 vex 
 |-  x e. _V
6 vex 
 |-  z e. _V
7 5 6 opelco 
 |-  ( <. x , z >. e. ( A o. B ) <-> E. y ( x B y /\ y A z ) )
8 df-br 
 |-  ( x C z <-> <. x , z >. e. C )
9 8 bicomi 
 |-  ( <. x , z >. e. C <-> x C z )
10 7 9 imbi12i 
 |-  ( ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) <-> ( E. y ( x B y /\ y A z ) -> x C z ) )
11 19.23v 
 |-  ( A. y ( ( x B y /\ y A z ) -> x C z ) <-> ( E. y ( x B y /\ y A z ) -> x C z ) )
12 10 11 bitr4i 
 |-  ( ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) <-> A. y ( ( x B y /\ y A z ) -> x C z ) )
13 12 albii 
 |-  ( A. z ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) <-> A. z A. y ( ( x B y /\ y A z ) -> x C z ) )
14 alcom 
 |-  ( A. z A. y ( ( x B y /\ y A z ) -> x C z ) <-> A. y A. z ( ( x B y /\ y A z ) -> x C z ) )
15 13 14 bitri 
 |-  ( A. z ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) <-> A. y A. z ( ( x B y /\ y A z ) -> x C z ) )
16 15 albii 
 |-  ( A. x A. z ( <. x , z >. e. ( A o. B ) -> <. x , z >. e. C ) <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) )
17 4 16 bitri 
 |-  ( ( A o. B ) C_ C <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) )