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∘B⊆C↔∀x∀y∀zxBy∧yAz→xCz

Proof

Step Hyp Ref Expression
1 relco ⊢Rel⁡A∘B
2 ssrel3 ⊢Rel⁡A∘B→A∘B⊆C↔∀x∀zxA∘Bz→xCz
3 1 2 ax-mp ⊢A∘B⊆C↔∀x∀zxA∘Bz→xCz
4 vex ⊢x∈V
5 vex ⊢z∈V
6 4 5 brco ⊢xA∘Bz↔∃yxBy∧yAz
7 6 imbi1i ⊢xA∘Bz→xCz↔∃yxBy∧yAz→xCz
8 19.23v ⊢∀yxBy∧yAz→xCz↔∃yxBy∧yAz→xCz
9 7 8 bitr4i ⊢xA∘Bz→xCz↔∀yxBy∧yAz→xCz
10 9 albii ⊢∀zxA∘Bz→xCz↔∀z∀yxBy∧yAz→xCz
11 breq2 ⊢z=w→yAz↔yAw
12 11 anbi2d ⊢z=w→xBy∧yAz↔xBy∧yAw
13 breq2 ⊢z=w→xCz↔xCw
14 12 13 imbi12d ⊢z=w→xBy∧yAz→xCz↔xBy∧yAw→xCw
15 breq2 ⊢y=w→xBy↔xBw
16 breq1 ⊢y=w→yAz↔wAz
17 15 16 anbi12d ⊢y=w→xBy∧yAz↔xBw∧wAz
18 17 imbi1d ⊢y=w→xBy∧yAz→xCz↔xBw∧wAz→xCz
19 14 18 alcomw ⊢∀z∀yxBy∧yAz→xCz↔∀y∀zxBy∧yAz→xCz
20 10 19 bitri ⊢∀zxA∘Bz→xCz↔∀y∀zxBy∧yAz→xCz
21 20 albii ⊢∀x∀zxA∘Bz→xCz↔∀x∀y∀zxBy∧yAz→xCz
22 3 21 bitri ⊢A∘B⊆C↔∀x∀y∀zxBy∧yAz→xCz