Metamath Proof Explorer

Theorem trpredeq2

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

Ref Expression
Assertion trpredeq2 
|- ( A = B -> TrPred ( R , A , X ) = TrPred ( R , B , X ) )

Proof

Step Hyp Ref Expression
1 predeq2 
 |-  ( A = B -> Pred ( R , A , y ) = Pred ( R , B , y ) )
2 1 iuneq2d 
 |-  ( A = B -> U_ y e. a Pred ( R , A , y ) = U_ y e. a Pred ( R , B , y ) )
3 2 mpteq2dv 
 |-  ( A = B -> ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) = ( a e. _V |-> U_ y e. a Pred ( R , B , y ) ) )
4 predeq2 
 |-  ( A = B -> Pred ( R , A , X ) = Pred ( R , B , X ) )
5 rdgeq12 
 |-  ( ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) = ( a e. _V |-> U_ y e. a Pred ( R , B , y ) ) /\ Pred ( R , A , X ) = Pred ( R , B , X ) ) -> 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 , B , y ) ) , Pred ( R , B , X ) ) )
6 5 reseq1d 
 |-  ( ( ( a e. _V |-> U_ y e. a Pred ( R , A , y ) ) = ( a e. _V |-> U_ y e. a Pred ( R , B , y ) ) /\ Pred ( R , A , X ) = Pred ( R , B , X ) ) -> ( 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 , B , y ) ) , Pred ( R , B , X ) ) |` _om ) )
7 3 4 6 syl2anc 
 |-  ( A = B -> ( 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 , B , y ) ) , Pred ( R , B , X ) ) |` _om ) )
8 7 rneqd 
 |-  ( A = B -> 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 , B , y ) ) , Pred ( R , B , X ) ) |` _om ) )
9 8 unieqd 
 |-  ( A = B -> 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 , B , y ) ) , Pred ( R , B , X ) ) |` _om ) )
10 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 )
11 df-trpred 
 |-  TrPred ( R , B , X ) = U. ran ( rec ( ( a e. _V |-> U_ y e. a Pred ( R , B , y ) ) , Pred ( R , B , X ) ) |` _om )
12 9 10 11 3eqtr4g 
 |-  ( A = B -> TrPred ( R , A , X ) = TrPred ( R , B , X ) )