Metamath Proof Explorer

Theorem trpredeq3

Description: Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011)

Ref Expression
Assertion trpredeq3 
|- ( X = Y -> TrPred ( R , A , X ) = TrPred ( R , A , Y ) )

Proof

Step Hyp Ref Expression
1 predeq3 
 |-  ( X = Y -> Pred ( R , A , X ) = Pred ( R , A , Y ) )
2 rdgeq2 
 |-  ( Pred ( R , A , X ) = Pred ( R , A , Y ) -> rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) = rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , Y ) ) )
3 1 2 syl 
 |-  ( X = Y -> rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) = rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , Y ) ) )
4 3 reseq1d 
 |-  ( X = Y -> ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) = ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , Y ) ) |` _om ) )
5 4 rneqd 
 |-  ( X = Y -> ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) = ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , Y ) ) |` _om ) )
6 5 unieqd 
 |-  ( X = Y -> U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , X ) ) |` _om ) = U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , Y ) ) |` _om ) )
7 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 )
8 df-trpred 
 |-  TrPred ( R , A , Y ) = U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) , Pred ( R , A , Y ) ) |` _om )
9 6 7 8 3eqtr4g 
 |-  ( X = Y -> TrPred ( R , A , X ) = TrPred ( R , A , Y ) )