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 C_ B -> ( R Or B -> R Or A ) )

Proof

Step	Hyp	Ref	Expression
1		poss	|- ( A C_ B -> ( R Po B -> R Po A ) )
2		ss2ralv	|- ( A C_ B -> ( A. x e. B A. y e. B ( x R y \/ x = y \/ y R x ) -> A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
3	1 2	anim12d	|- ( A C_ B -> ( ( R Po B /\ A. x e. B A. y e. B ( x R y \/ x = y \/ y R x ) ) -> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) ) )
4		df-so	|- ( R Or B <-> ( R Po B /\ A. x e. B A. y e. B ( x R y \/ x = y \/ y R x ) ) )
5		df-so	|- ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
6	3 4 5	3imtr4g	|- ( A C_ B -> ( R Or B -> R Or A ) )