Metamath Proof Explorer


Theorem eltrpred

Description: A class is a transitive predecessor iff it is in some value of the underlying function. This theorem is not meant to be used directly; use trpredpred and trpredmintr instead. (Contributed by Scott Fenton, 28-Apr-2012)

Ref Expression
Assertion eltrpred
|- ( Y e. TrPred ( R , A , X ) <-> E. i e. _om Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) )

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 1 eleq2i
 |-  ( Y e. TrPred ( R , A , X ) <-> Y e. U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) )
3 eliun
 |-  ( Y e. U_ i e. _om ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) <-> E. i e. _om Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) )
4 2 3 bitri
 |-  ( Y e. TrPred ( R , A , X ) <-> E. i e. _om Y e. ( ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) ` i ) )