coss12d

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

Step	Hyp	Ref	Expression
1		coss12d.a	$⊢ φ \to A \subseteq B$
2		coss12d.c	$⊢ φ \to C \subseteq D$
3	2	ssbrd	$⊢ φ \to (x C y \to x D y)$
4	1	ssbrd	$⊢ φ \to (y A z \to y B z)$
5	3 4	anim12d	$⊢ φ \to ((x C y \land y A z) \to (x D y \land y B z))$
6	5	eximdv	$⊢ φ \to (\exists y (x C y \land y A z) \to \exists y (x D y \land y B z))$
7	6	ssopab2dv	$⊢ φ \to \{⟨x, z⟩ \| \exists y (x C y \land y A z)\} \subseteq \{⟨x, z⟩ \| \exists y (x D y \land y B z)\}$
8		df-co	$⊢ A \circ C = \{⟨x, z⟩ \| \exists y (x C y \land y A z)\}$
9		df-co	$⊢ B \circ D = \{⟨x, z⟩ \| \exists y (x D y \land y B z)\}$
10	7 8 9	3sstr4g	$⊢ φ \to A \circ C \subseteq B \circ D$

Metamath Proof Explorer