Metamath Proof Explorer

Theorem trpredelss

Description: Given a transitive predecessor Y of X , the transitive predecessors of Y form a subclass of the transitive predecessors of X . (Contributed by Scott Fenton, 25-Apr-2012) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	trpredelss	$⊢ (X \in A \land R Se A) \to (Y \in TrPred (R, A, X) \to TrPred (R, A, Y) \subseteq TrPred (R, A, X))$

Proof

Step	Hyp	Ref	Expression
1		setlikespec	$⊢ (X \in A \land R Se A) \to Pred (R, A, X) \in V$
2		trpredss	$⊢ Pred (R, A, X) \in V \to TrPred (R, A, X) \subseteq A$
3	1 2	syl	$⊢ (X \in A \land R Se A) \to TrPred (R, A, X) \subseteq A$
4	3	sselda	$⊢ ((X \in A \land R Se A) \land Y \in TrPred (R, A, X)) \to Y \in A$
5		simplr	$⊢ ((X \in A \land R Se A) \land Y \in TrPred (R, A, X)) \to R Se A$
6		trpredtr	$⊢ (X \in A \land R Se A) \to (y \in TrPred (R, A, X) \to Pred (R, A, y) \subseteq TrPred (R, A, X))$
7	6	ralrimiv	$⊢ (X \in A \land R Se A) \to \forall y \in TrPred (R, A, X) Pred (R, A, y) \subseteq TrPred (R, A, X)$
8	7	adantr	$⊢ ((X \in A \land R Se A) \land Y \in TrPred (R, A, X)) \to \forall y \in TrPred (R, A, X) Pred (R, A, y) \subseteq TrPred (R, A, X)$
9		trpredtr	$⊢ (X \in A \land R Se A) \to (Y \in TrPred (R, A, X) \to Pred (R, A, Y) \subseteq TrPred (R, A, X))$
10	9	imp	$⊢ ((X \in A \land R Se A) \land Y \in TrPred (R, A, X)) \to Pred (R, A, Y) \subseteq TrPred (R, A, X)$
11		trpredmintr	$⊢ ((Y \in A \land R Se A) \land (\forall y \in TrPred (R, A, X) Pred (R, A, y) \subseteq TrPred (R, A, X) \land Pred (R, A, Y) \subseteq TrPred (R, A, X))) \to TrPred (R, A, Y) \subseteq TrPred (R, A, X)$
12	4 5 8 10 11	syl22anc	$⊢ ((X \in A \land R Se A) \land Y \in TrPred (R, A, X)) \to TrPred (R, A, Y) \subseteq TrPred (R, A, X)$
13	12	ex	$⊢ (X \in A \land R Se A) \to (Y \in TrPred (R, A, X) \to TrPred (R, A, Y) \subseteq TrPred (R, A, X))$