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 ( ( 𝐴 ∘ 𝐵 ) ⊆ 𝐶 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )

Proof

Step Hyp Ref Expression
1 relco ⊢ Rel ( 𝐴 ∘ 𝐵 )
2 ssrel3 ⊢ ( Rel ( 𝐴 ∘ 𝐵 ) → ( ( 𝐴 ∘ 𝐵 ) ⊆ 𝐶 ↔ ∀ 𝑥 ∀ 𝑧 ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑧 → 𝑥 𝐶 𝑧 ) ) )
3 1 2 ax-mp ⊢ ( ( 𝐴 ∘ 𝐵 ) ⊆ 𝐶 ↔ ∀ 𝑥 ∀ 𝑧 ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑧 → 𝑥 𝐶 𝑧 ) )
4 vex ⊢ 𝑥 ∈ V
5 vex ⊢ 𝑧 ∈ V
6 4 5 brco ⊢ ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑧 ↔ ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) )
7 6 imbi1i ⊢ ( ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑧 → 𝑥 𝐶 𝑧 ) ↔ ( ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )
8 19.23v ⊢ ( ∀ 𝑦 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ↔ ( ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )
9 7 8 bitr4i ⊢ ( ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑧 → 𝑥 𝐶 𝑧 ) ↔ ∀ 𝑦 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )
10 9 albii ⊢ ( ∀ 𝑧 ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑧 → 𝑥 𝐶 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )
11 breq2 ⊢ ( 𝑧 = 𝑤 → ( 𝑦 𝐴 𝑧 ↔ 𝑦 𝐴 𝑤 ) )
12 11 anbi2d ⊢ ( 𝑧 = 𝑤 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ↔ ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑤 ) ) )
13 breq2 ⊢ ( 𝑧 = 𝑤 → ( 𝑥 𝐶 𝑧 ↔ 𝑥 𝐶 𝑤 ) )
14 12 13 imbi12d ⊢ ( 𝑧 = 𝑤 → ( ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ↔ ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑤 ) → 𝑥 𝐶 𝑤 ) ) )
15 breq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑥 𝐵 𝑦 ↔ 𝑥 𝐵 𝑤 ) )
16 breq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 𝐴 𝑧 ↔ 𝑤 𝐴 𝑧 ) )
17 15 16 anbi12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) ↔ ( 𝑥 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) ) )
18 17 imbi1d ⊢ ( 𝑦 = 𝑤 → ( ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ↔ ( ( 𝑥 𝐵 𝑤 ∧ 𝑤 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ) )
19 14 18 alcomw ⊢ ( ∀ 𝑧 ∀ 𝑦 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )
20 10 19 bitri ⊢ ( ∀ 𝑧 ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑧 → 𝑥 𝐶 𝑧 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )
21 20 albii ⊢ ( ∀ 𝑥 ∀ 𝑧 ( 𝑥 ( 𝐴 ∘ 𝐵 ) 𝑧 → 𝑥 𝐶 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )
22 3 21 bitri ⊢ ( ( 𝐴 ∘ 𝐵 ) ⊆ 𝐶 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐴 𝑧 ) → 𝑥 𝐶 𝑧 ) )