Theorem cossss

Description: Subclass theorem for the classes of cosets by A and B . (Contributed by Peter Mazsa, 11-Nov-2019)

	Ref	Expression
Assertion	cossss	$$⊢A\subseteq B\to \wr A\subseteq \wr B$$

Proof

Step	Hyp	Ref	Expression
1		ssbr	$$⊢A\subseteq B\to \left(xAy\to xBy\right)$$
2		ssbr	$$⊢A\subseteq B\to \left(xAz\to xBz\right)$$
3	1 2	anim12d	$$⊢A\subseteq B\to \left(\left(xAy\wedge xAz\right)\to \left(xBy\wedge xBz\right)\right)$$
4	3	eximdv	$$⊢A\subseteq B\to \left(\exists x\left(xAy\wedge xAz\right)\to \exists x\left(xBy\wedge xBz\right)\right)$$
5	4	ssopab2dv	$$⊢A\subseteq B\to \left\{⟨y,z⟩|\exists x\left(xAy\wedge xAz\right)\right\}\subseteq \left\{⟨y,z⟩|\exists x\left(xBy\wedge xBz\right)\right\}$$
6		df-coss	$$⊢\wr A=\left\{⟨y,z⟩|\exists x\left(xAy\wedge xAz\right)\right\}$$
7		df-coss	$$⊢\wr B=\left\{⟨y,z⟩|\exists x\left(xBy\wedge xBz\right)\right\}$$
8	5 6 7	3sstr4g	$$⊢A\subseteq B\to \wr A\subseteq \wr B$$