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 B C x y z x B y y A z x C z

Proof

Step Hyp Ref Expression
1 df-co A B = x z | y x B y y A z
2 1 relopabiv Rel A B
3 ssrel Rel A B A B C x z x z A B x z C
4 2 3 ax-mp A B C x z x z A B x z C
5 vex x V
6 vex z V
7 5 6 opelco x z A B y x B y y A z
8 df-br x C z x z C
9 8 bicomi x z C x C z
10 7 9 imbi12i x z A B x z C y x B y y A z x C z
11 19.23v y x B y y A z x C z y x B y y A z x C z
12 10 11 bitr4i x z A B x z C y x B y y A z x C z
13 12 albii z x z A B x z C z y x B y y A z x C z
14 alcom z y x B y y A z x C z y z x B y y A z x C z
15 13 14 bitri z x z A B x z C y z x B y y A z x C z
16 15 albii x z x z A B x z C x y z x B y y A z x C z
17 4 16 bitri A B C x y z x B y y A z x C z