Theorem coss2

Description: Subclass theorem for composition. (Contributed by NM, 5-Apr-2013)

	Ref	Expression
Assertion	coss2	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∘ 𝐴 ) ⊆ ( 𝐶 ∘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ssbr	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑦 ) )
2	1	anim1d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑥 𝐴 𝑦 ∧ 𝑦 𝐶 𝑧 ) → ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐶 𝑧 ) ) )
3	2	eximdv	⊢ ( 𝐴 ⊆ 𝐵 → ( ∃ 𝑦 ( 𝑥 𝐴 𝑦 ∧ 𝑦 𝐶 𝑧 ) → ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐶 𝑧 ) ) )
4	3	ssopab2dv	⊢ ( 𝐴 ⊆ 𝐵 → { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐴 𝑦 ∧ 𝑦 𝐶 𝑧 ) } ⊆ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐶 𝑧 ) } )
5		df-co	⊢ ( 𝐶 ∘ 𝐴 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐴 𝑦 ∧ 𝑦 𝐶 𝑧 ) }
6		df-co	⊢ ( 𝐶 ∘ 𝐵 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐵 𝑦 ∧ 𝑦 𝐶 𝑧 ) }
7	4 5 6	3sstr4g	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∘ 𝐴 ) ⊆ ( 𝐶 ∘ 𝐵 ) )