This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 relco ⊢ Rel ⁡ A ∘ B
2 ssrel3 ⊢ Rel ⁡ A ∘ B → A ∘ B ⊆ C ↔ ∀ x ∀ z x A ∘ B z → x C z
3 1 2 ax-mp ⊢ A ∘ B ⊆ C ↔ ∀ x ∀ z x A ∘ B z → x C z
4 vex ⊢ x ∈ V
5 vex ⊢ z ∈ V
6 4 5 brco ⊢ x A ∘ B z ↔ ∃ y x B y ∧ y A z
7 6 imbi1i ⊢ x A ∘ B z → x C z ↔ ∃ y x B y ∧ y A z → x C z
8 19.23v ⊢ ∀ y x B y ∧ y A z → x C z ↔ ∃ y x B y ∧ y A z → x C z
9 7 8 bitr4i ⊢ x A ∘ B z → x C z ↔ ∀ y x B y ∧ y A z → x C z
10 9 albii ⊢ ∀ z x A ∘ B z → x C z ↔ ∀ z ∀ 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 ⊢ ∀ z ∀ y x B y ∧ y A z → x C z ↔ ∀ y ∀ z x B y ∧ y A z → x C z
20 10 19 bitri ⊢ ∀ z x A ∘ B z → x C z ↔ ∀ y ∀ z x B y ∧ y A z → x C z
21 20 albii ⊢ ∀ x ∀ z x A ∘ B z → x C z ↔ ∀ x ∀ y ∀ z x B y ∧ y A z → x C z
22 3 21 bitri ⊢ A ∘ B ⊆ C ↔ ∀ x ∀ y ∀ z x B y ∧ y A z → x C z