Metamath Proof Explorer

Theorem cotrgOLDOLD

Description: Obsolete version of cotrg as of 19-Dec-2024. (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 modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cotrgOLDOLD ⊢A∘B⊆C↔∀x∀y∀zxBy∧yAz→xCz

Proof

Step Hyp Ref Expression
1 relco ⊢Rel⁡A∘B
2 ssrel ⊢Rel⁡A∘B→A∘B⊆C↔∀x∀zxz∈A∘B→xz∈C
3 1 2 ax-mp ⊢A∘B⊆C↔∀x∀zxz∈A∘B→xz∈C
4 vex ⊢x∈V
5 vex ⊢z∈V
6 4 5 opelco ⊢xz∈A∘B↔∃yxBy∧yAz
7 df-br ⊢xCz↔xz∈C
8 7 bicomi ⊢xz∈C↔xCz
9 6 8 imbi12i ⊢xz∈A∘B→xz∈C↔∃yxBy∧yAz→xCz
10 19.23v ⊢∀yxBy∧yAz→xCz↔∃yxBy∧yAz→xCz
11 9 10 bitr4i ⊢xz∈A∘B→xz∈C↔∀yxBy∧yAz→xCz
12 11 albii ⊢∀zxz∈A∘B→xz∈C↔∀z∀yxBy∧yAz→xCz
13 alcom ⊢∀z∀yxBy∧yAz→xCz↔∀y∀zxBy∧yAz→xCz
14 12 13 bitri ⊢∀zxz∈A∘B→xz∈C↔∀y∀zxBy∧yAz→xCz
15 14 albii ⊢∀x∀zxz∈A∘B→xz∈C↔∀x∀y∀zxBy∧yAz→xCz
16 3 15 bitri ⊢A∘B⊆C↔∀x∀y∀zxBy∧yAz→xCz