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 |