Metamath Proof Explorer


Theorem dftrpred2

Description: A definition of the transitive predecessors of a class in terms of indexed union. (Contributed by Scott Fenton, 28-Apr-2012)

Ref Expression
Assertion 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 )

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 fniunfv
 |-  ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) Fn _om -> U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) = U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) )
4 2 3 ax-mp
 |-  U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) = U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om )
5 1 4 eqtr4i
 |-  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 )