Theorem predso

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

	Ref	Expression
Assertion	predso	$$⊢\left(R\mathrm{Or}A\wedge X\in A\right)\to \left(Y\in Pred\left(R,A,X\right)\to Pred\left(R,A,Y\right)\subseteq Pred\left(R,A,X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sopo	$$⊢R\mathrm{Or}A\to R\mathrm{Po}A$$
2		predpo	$$⊢\left(R\mathrm{Po}A\wedge X\in A\right)\to \left(Y\in Pred\left(R,A,X\right)\to Pred\left(R,A,Y\right)\subseteq Pred\left(R,A,X\right)\right)$$
3	1 2	sylan	$$⊢\left(R\mathrm{Or}A\wedge X\in A\right)\to \left(Y\in Pred\left(R,A,X\right)\to Pred\left(R,A,Y\right)\subseteq Pred\left(R,A,X\right)\right)$$