Theorem soss

Description: Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	soss	$$⊢A\subseteq B\to \left(R\mathrm{Or}B\to R\mathrm{Or}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		poss	$$⊢A\subseteq B\to \left(R\mathrm{Po}B\to R\mathrm{Po}A\right)$$
2		ss2ralv	$$⊢A\subseteq B\to \left(\forall x\in B\forall y\in B\left(xRy\vee x=y\vee yRx\right)\to \forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\right)$$
3	1 2	anim12d	$$⊢A\subseteq B\to \left(\left(R\mathrm{Po}B\wedge \forall x\in B\forall y\in B\left(xRy\vee x=y\vee yRx\right)\right)\to \left(R\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\right)\right)$$
4		df-so	$$⊢R\mathrm{Or}B\leftrightarrow \left(R\mathrm{Po}B\wedge \forall x\in B\forall y\in B\left(xRy\vee x=y\vee yRx\right)\right)$$
5		df-so	$$⊢R\mathrm{Or}A\leftrightarrow \left(R\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\right)$$
6	3 4 5	3imtr4g	$$⊢A\subseteq B\to \left(R\mathrm{Or}B\to R\mathrm{Or}A\right)$$