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	⊢ ( 𝜑 → ( 𝐴 ∘ 𝐶 ) ⊆ ( 𝐵 ∘ 𝐷 ) )