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 e. A /\ R Se A ) -> ( Y e. TrPred ( R , A , X ) -> TrPred ( R , A , Y ) C_ TrPred ( R , A , X ) ) )

Proof

Step	Hyp	Ref	Expression
1		setlikespec	|- ( ( X e. A /\ R Se A ) -> Pred ( R , A , X ) e. _V )
2		trpredss	|- ( Pred ( R , A , X ) e. _V -> TrPred ( R , A , X ) C_ A )
3	1 2	syl	|- ( ( X e. A /\ R Se A ) -> TrPred ( R , A , X ) C_ A )
4	3	sselda	|- ( ( ( X e. A /\ R Se A ) /\ Y e. TrPred ( R , A , X ) ) -> Y e. A )
5		simplr	|- ( ( ( X e. A /\ R Se A ) /\ Y e. TrPred ( R , A , X ) ) -> R Se A )
6		trpredtr	|- ( ( X e. A /\ R Se A ) -> ( y e. TrPred ( R , A , X ) -> Pred ( R , A , y ) C_ TrPred ( R , A , X ) ) )
7	6	ralrimiv	|- ( ( X e. A /\ R Se A ) -> A. y e. TrPred ( R , A , X ) Pred ( R , A , y ) C_ TrPred ( R , A , X ) )
8	7	adantr	|- ( ( ( X e. A /\ R Se A ) /\ Y e. TrPred ( R , A , X ) ) -> A. y e. TrPred ( R , A , X ) Pred ( R , A , y ) C_ TrPred ( R , A , X ) )
9		trpredtr	|- ( ( X e. A /\ R Se A ) -> ( Y e. TrPred ( R , A , X ) -> Pred ( R , A , Y ) C_ TrPred ( R , A , X ) ) )
10	9	imp	|- ( ( ( X e. A /\ R Se A ) /\ Y e. TrPred ( R , A , X ) ) -> Pred ( R , A , Y ) C_ TrPred ( R , A , X ) )
11		trpredmintr	|- ( ( ( Y e. A /\ R Se A ) /\ ( A. y e. TrPred ( R , A , X ) Pred ( R , A , y ) C_ TrPred ( R , A , X ) /\ Pred ( R , A , Y ) C_ TrPred ( R , A , X ) ) ) -> TrPred ( R , A , Y ) C_ TrPred ( R , A , X ) )
12	4 5 8 10 11	syl22anc	|- ( ( ( X e. A /\ R Se A ) /\ Y e. TrPred ( R , A , X ) ) -> TrPred ( R , A , Y ) C_ TrPred ( R , A , X ) )
13	12	ex	|- ( ( X e. A /\ R Se A ) -> ( Y e. TrPred ( R , A , X ) -> TrPred ( R , A , Y ) C_ TrPred ( R , A , X ) ) )