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