Metamath Proof Explorer

Theorem predso

Description: Property of the predecessor class for strict total orders. (Contributed by Scott Fenton, 11-Feb-2011)

		Ref	Expression
	Assertion	predso	\|- ( ( R Or A /\ X e. A ) -> ( Y e. Pred ( R , A , X ) -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) ) )

Step	Hyp	Ref	Expression
1		sopo	\|- ( R Or A -> R Po A )
2		predpo	\|- ( ( R Po A /\ X e. A ) -> ( Y e. Pred ( R , A , X ) -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) ) )
3	1 2	sylan	\|- ( ( R Or A /\ X e. A ) -> ( Y e. Pred ( R , A , X ) -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) ) )

Step

Hyp

Ref

Expression

 |-  ( R Or A -> R Po A )

 |-  ( ( R Po A /\ X e. A ) -> ( Y e. Pred ( R , A , X ) -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) ) )

1 2

 |-  ( ( R Or A /\ X e. A ) -> ( Y e. Pred ( R , A , X ) -> Pred ( R , A , Y ) C_ Pred ( R , A , X ) ) )