Theorem trpredss

Description: The transitive predecessors form a subset of the base class. (Contributed by Scott Fenton, 20-Feb-2011)

	Ref	Expression
Assertion	trpredss	|- ( Pred ( R , A , X ) e. B -> TrPred ( R , A , X ) C_ A )

Proof

Step	Hyp	Ref	Expression
1		dftrpred2	|- TrPred ( R , A , X ) = U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i )
2		trpredlem1	|- ( Pred ( R , A , X ) e. B -> ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A )
3	2	ralrimivw	|- ( Pred ( R , A , X ) e. B -> A. i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A )
4		iunss	|- ( U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A <-> A. i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A )
5	3 4	sylibr	|- ( Pred ( R , A , X ) e. B -> U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) C_ A )
6	1 5	eqsstrid	|- ( Pred ( R , A , X ) e. B -> TrPred ( R , A , X ) C_ A )