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

Metamath Proof Explorer

Theorem coss12d

Description: Subset deduction for composition of two classes. (Contributed by RP, 24-Dec-2019)

Ref Expression
Hypotheses coss12d.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
coss12d.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐷 )
Assertion coss12d ( 𝜑 → ( 𝐴 ∘ 𝐶 ) ⊆ ( 𝐵 ∘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 coss12d.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2 coss12d.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐷 )
3 2 ssbrd ⊢ ( 𝜑 → ( 𝑥 𝐶 𝑦 → 𝑥 𝐷 𝑦 ) )
4 1 ssbrd ⊢ ( 𝜑 → ( 𝑦 𝐴 𝑧 → 𝑦 𝐵 𝑧 ) )
5 3 4 anim12d ⊢ ( 𝜑 → ( ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) → ( 𝑥 𝐷 𝑦 ∧ 𝑦 𝐵 𝑧 ) ) )
6 5 eximdv ⊢ ( 𝜑 → ( ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) → ∃ 𝑦 ( 𝑥 𝐷 𝑦 ∧ 𝑦 𝐵 𝑧 ) ) )
7 6 ssopab2dv ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) } ⊆ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐷 𝑦 ∧ 𝑦 𝐵 𝑧 ) } )
8 df-co ⊢ ( 𝐴 ∘ 𝐶 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐶 𝑦 ∧ 𝑦 𝐴 𝑧 ) }
9 df-co ⊢ ( 𝐵 ∘ 𝐷 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐷 𝑦 ∧ 𝑦 𝐵 𝑧 ) }
10 7 8 9 3sstr4g ⊢ ( 𝜑 → ( 𝐴 ∘ 𝐶 ) ⊆ ( 𝐵 ∘ 𝐷 ) )