Theorem trpredex

Description: The transitive predecessors under a relation form a set.

This is the first theorem in the transitive predecessor series that requires the axiom of infinity. (Contributed by Scott Fenton, 18-Feb-2011)

	Ref	Expression
Assertion	trpredex	|- TrPred ( R , A , X ) e. _V

Proof

Step	Hyp	Ref	Expression
1		df-trpred	|- TrPred ( R , A , X ) = U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om )
2		frfnom	|- ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Fn _om
3		omex	|- _om e. _V
4		fnex	|- ( ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Fn _om /\ _om e. _V ) -> ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) e. _V )
5	2 3 4	mp2an	|- ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) e. _V
6	5	rnex	|- ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) e. _V
7	6	uniex	|- U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) e. _V
8	1 7	eqeltri	|- TrPred ( R , A , X ) e. _V