Metamath Proof Explorer

Theorem trpredpo

Description: If R partially orders A , then the transitive predecessors are the same as the immediate predecessors . (Contributed by Scott Fenton, 28-Apr-2012) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	trpredpo	$⊢ (R Po A \land X \in A \land R Se A) \to TrPred (R, A, X) = Pred (R, A, X)$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (R Po A \land X \in A \land R Se A) \to X \in A$
2		simp3	$⊢ (R Po A \land X \in A \land R Se A) \to R Se A$
3		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))$
4	3	ralrimiv	$⊢ (R Po A \land X \in A) \to \forall y \in Pred (R, A, X) Pred (R, A, y) \subseteq Pred (R, A, X)$
5	4	3adant3	$⊢ (R Po A \land X \in A \land R Se A) \to \forall y \in Pred (R, A, X) Pred (R, A, y) \subseteq Pred (R, A, X)$
6		ssidd	$⊢ (R Po A \land X \in A \land R Se A) \to Pred (R, A, X) \subseteq Pred (R, A, X)$
7		trpredmintr	$⊢ ((X \in A \land R Se A) \land (\forall y \in Pred (R, A, X) Pred (R, A, y) \subseteq Pred (R, A, X) \land Pred (R, A, X) \subseteq Pred (R, A, X))) \to TrPred (R, A, X) \subseteq Pred (R, A, X)$
8	1 2 5 6 7	syl22anc	$⊢ (R Po A \land X \in A \land R Se A) \to TrPred (R, A, X) \subseteq Pred (R, A, X)$
9		setlikespec	$⊢ (X \in A \land R Se A) \to Pred (R, A, X) \in V$
10		trpredpred	$⊢ Pred (R, A, X) \in V \to Pred (R, A, X) \subseteq TrPred (R, A, X)$
11	9 10	syl	$⊢ (X \in A \land R Se A) \to Pred (R, A, X) \subseteq TrPred (R, A, X)$
12	11	3adant1	$⊢ (R Po A \land X \in A \land R Se A) \to Pred (R, A, X) \subseteq TrPred (R, A, X)$
13	8 12	eqssd	$⊢ (R Po A \land X \in A \land R Se A) \to TrPred (R, A, X) = Pred (R, A, X)$