predpo

Description: Property of the precessor class for partial orderings. (Contributed by Scott Fenton, 28-Apr-2012)

		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		predel	$⊢ Y \in Pred (R, A, X) \to Y \in A$
2		elpredg	$⊢ (X \in A \land Y \in A) \to (Y \in Pred (R, A, X) \leftrightarrow Y R X)$
3	2	adantll	$⊢ ((R Po A \land X \in A) \land Y \in A) \to (Y \in Pred (R, A, X) \leftrightarrow Y R X)$
4		potr	$⊢ (R Po A \land (z \in A \land Y \in A \land X \in A)) \to ((z R Y \land Y R X) \to z R X)$
5	4	3exp2	$⊢ R Po A \to (z \in A \to (Y \in A \to (X \in A \to ((z R Y \land Y R X) \to z R X))))$
6	5	com24	$⊢ R Po A \to (X \in A \to (Y \in A \to (z \in A \to ((z R Y \land Y R X) \to z R X))))$
7	6	imp31	$⊢ ((R Po A \land X \in A) \land Y \in A) \to (z \in A \to ((z R Y \land Y R X) \to z R X))$
8	7	com13	$⊢ (z R Y \land Y R X) \to (z \in A \to (((R Po A \land X \in A) \land Y \in A) \to z R X))$
9	8	ex	$⊢ z R Y \to (Y R X \to (z \in A \to (((R Po A \land X \in A) \land Y \in A) \to z R X)))$
10	9	com14	$⊢ ((R Po A \land X \in A) \land Y \in A) \to (Y R X \to (z \in A \to (z R Y \to z R X)))$
11	3 10	sylbid	$⊢ ((R Po A \land X \in A) \land Y \in A) \to (Y \in Pred (R, A, X) \to (z \in A \to (z R Y \to z R X)))$
12	11	ex	$⊢ (R Po A \land X \in A) \to (Y \in A \to (Y \in Pred (R, A, X) \to (z \in A \to (z R Y \to z R X))))$
13	12	com23	$⊢ (R Po A \land X \in A) \to (Y \in Pred (R, A, X) \to (Y \in A \to (z \in A \to (z R Y \to z R X))))$
14	13	3imp	$⊢ ((R Po A \land X \in A) \land Y \in Pred (R, A, X) \land Y \in A) \to (z \in A \to (z R Y \to z R X))$
15	14	imdistand	$⊢ ((R Po A \land X \in A) \land Y \in Pred (R, A, X) \land Y \in A) \to ((z \in A \land z R Y) \to (z \in A \land z R X))$
16		vex	$⊢ z \in V$
17	16	elpred	$⊢ Y \in A \to (z \in Pred (R, A, Y) \leftrightarrow (z \in A \land z R Y))$
18	17	3ad2ant3	$⊢ ((R Po A \land X \in A) \land Y \in Pred (R, A, X) \land Y \in A) \to (z \in Pred (R, A, Y) \leftrightarrow (z \in A \land z R Y))$
19	16	elpred	$⊢ X \in A \to (z \in Pred (R, A, X) \leftrightarrow (z \in A \land z R X))$
20	19	adantl	$⊢ (R Po A \land X \in A) \to (z \in Pred (R, A, X) \leftrightarrow (z \in A \land z R X))$
21	20	3ad2ant1	$⊢ ((R Po A \land X \in A) \land Y \in Pred (R, A, X) \land Y \in A) \to (z \in Pred (R, A, X) \leftrightarrow (z \in A \land z R X))$
22	15 18 21	3imtr4d	$⊢ ((R Po A \land X \in A) \land Y \in Pred (R, A, X) \land Y \in A) \to (z \in Pred (R, A, Y) \to z \in Pred (R, A, X))$
23	22	ssrdv	$⊢ ((R Po A \land X \in A) \land Y \in Pred (R, A, X) \land Y \in A) \to Pred (R, A, Y) \subseteq Pred (R, A, X)$
24	23	3exp	$⊢ (R Po A \land X \in A) \to (Y \in Pred (R, A, X) \to (Y \in A \to Pred (R, A, Y) \subseteq Pred (R, A, X)))$
25	1 24	mpdi	$⊢ (R Po A \land X \in A) \to (Y \in Pred (R, A, X) \to Pred (R, A, Y) \subseteq Pred (R, A, X))$

Metamath Proof Explorer

Theorem predpo

Proof