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

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 \land X \in A) \to (Y \in Pred (R, A, X) \to Pred (R, A, Y) \subseteq Pred (R, A, X))$

Step	Hyp	Ref	Expression
1		sopo	$⊢ R Or A \to R Po A$
2		predpo	$⊢ (R Po A \land X \in A) \to (Y \in Pred (R, A, X) \to Pred (R, A, Y) \subseteq Pred (R, A, X))$
3	1 2	sylan	$⊢ (R Or A \land X \in A) \to (Y \in Pred (R, A, X) \to Pred (R, A, Y) \subseteq Pred (R, A, X))$