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