Metamath Proof Explorer

Theorem predpo

Description: Property of the predecessor class for partial orders. (Contributed by Scott Fenton, 28-Apr-2012) (Proof shortened by Scott Fenton, 28-Oct-2024)

		Ref	Expression
	Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		dfpo2	$⊢ R Po A \leftrightarrow (R \cap ({I ↾}_{A}) = \emptyset \land (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R)$
2	1	simprbi	$⊢ R Po A \to (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R$
3	2	ad2antrr	$⊢ ((R Po A \land X \in A) \land Y \in Pred (R, A, X)) \to (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R$
4		simpr	$⊢ ((R Po A \land X \in A) \land Y \in Pred (R, A, X)) \to Y \in Pred (R, A, X)$
5		simplr	$⊢ ((R Po A \land X \in A) \land Y \in Pred (R, A, X)) \to X \in A$
6		predtrss	$⊢ ((R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \land Y \in Pred (R, A, X) \land X \in A) \to Pred (R, A, Y) \subseteq Pred (R, A, X)$
7	3 4 5 6	syl3anc	$⊢ ((R Po A \land X \in A) \land Y \in Pred (R, A, X)) \to Pred (R, A, Y) \subseteq Pred (R, A, X)$
8	7	ex	$⊢ (R Po A \land X \in A) \to (Y \in Pred (R, A, X) \to Pred (R, A, Y) \subseteq Pred (R, A, X))$