This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )