Metamath Proof Explorer

Theorem poss

Description: Subset theorem for the partial ordering predicate. (Contributed by NM, 27-Mar-1997) (Proof shortened by Mario Carneiro, 18-Nov-2016)

Ref Expression
Assertion poss 
|- ( A C_ B -> ( R Po B -> R Po A ) )

Proof

Step Hyp Ref Expression
1 ssralv 
 |-  ( A C_ B -> ( A. x e. B A. y e. B A. z e. B ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) -> A. x e. A A. y e. B A. z e. B ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
2 ss2ralv 
 |-  ( A C_ B -> ( A. y e. B A. z e. B ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) -> A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
3 2 ralimdv 
 |-  ( A C_ B -> ( A. x e. A A. y e. B A. z e. B ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) -> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
4 1 3 syld 
 |-  ( A C_ B -> ( A. x e. B A. y e. B A. z e. B ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) -> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
5 df-po 
 |-  ( R Po B <-> A. x e. B A. y e. B A. z e. B ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )
6 df-po 
 |-  ( R Po A <-> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )
7 4 5 6 3imtr4g 
 |-  ( A C_ B -> ( R Po B -> R Po A ) )