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) (Proof shortened by SN, 19-Dec-2024) Avoid ax-11 . (Revised by BTernaryTau, 29-Dec-2024)

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 relco 
 |-  Rel ( A o. B )
2 ssrel3 
 |-  ( Rel ( A o. B ) -> ( ( A o. B ) C_ C <-> A. x A. z ( x ( A o. B ) z -> x C z ) ) )
3 1 2 ax-mp 
 |-  ( ( A o. B ) C_ C <-> A. x A. z ( x ( A o. B ) z -> x C z ) )
4 vex 
 |-  x e. _V
5 vex 
 |-  z e. _V
6 4 5 brco 
 |-  ( x ( A o. B ) z <-> E. y ( x B y /\ y A z ) )
7 6 imbi1i 
 |-  ( ( x ( A o. B ) z -> x C z ) <-> ( E. y ( x B y /\ y A z ) -> x C z ) )
8 19.23v 
 |-  ( A. y ( ( x B y /\ y A z ) -> x C z ) <-> ( E. y ( x B y /\ y A z ) -> x C z ) )
9 7 8 bitr4i 
 |-  ( ( x ( A o. B ) z -> x C z ) <-> A. y ( ( x B y /\ y A z ) -> x C z ) )
10 9 albii 
 |-  ( A. z ( x ( A o. B ) z -> x C z ) <-> A. z A. y ( ( x B y /\ y A z ) -> x C z ) )
11 breq2 
 |-  ( z = w -> ( y A z <-> y A w ) )
12 11 anbi2d 
 |-  ( z = w -> ( ( x B y /\ y A z ) <-> ( x B y /\ y A w ) ) )
13 breq2 
 |-  ( z = w -> ( x C z <-> x C w ) )
14 12 13 imbi12d 
 |-  ( z = w -> ( ( ( x B y /\ y A z ) -> x C z ) <-> ( ( x B y /\ y A w ) -> x C w ) ) )
15 breq2 
 |-  ( y = w -> ( x B y <-> x B w ) )
16 breq1 
 |-  ( y = w -> ( y A z <-> w A z ) )
17 15 16 anbi12d 
 |-  ( y = w -> ( ( x B y /\ y A z ) <-> ( x B w /\ w A z ) ) )
18 17 imbi1d 
 |-  ( y = w -> ( ( ( x B y /\ y A z ) -> x C z ) <-> ( ( x B w /\ w A z ) -> x C z ) ) )
19 14 18 alcomw 
 |-  ( 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 ) )
20 10 19 bitri 
 |-  ( A. z ( x ( A o. B ) z -> x C z ) <-> A. y A. z ( ( x B y /\ y A z ) -> x C z ) )
21 20 albii 
 |-  ( A. x A. z ( x ( A o. B ) z -> x C z ) <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) )
22 3 21 bitri 
 |-  ( ( A o. B ) C_ C <-> A. x A. y A. z ( ( x B y /\ y A z ) -> x C z ) )