Metamath Proof Explorer

Theorem wrecseq123

Description: General equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018)

Ref Expression
Assertion wrecseq123 
|- ( ( R = S /\ A = B /\ F = G ) -> wrecs ( R , A , F ) = wrecs ( S , B , G ) )

Proof

Step Hyp Ref Expression
1 sseq2 
 |-  ( A = B -> ( x C_ A <-> x C_ B ) )
2 1 3ad2ant2 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( x C_ A <-> x C_ B ) )
3 predeq1 
 |-  ( R = S -> Pred ( R , A , y ) = Pred ( S , A , y ) )
4 predeq2 
 |-  ( A = B -> Pred ( S , A , y ) = Pred ( S , B , y ) )
5 3 4 sylan9eq 
 |-  ( ( R = S /\ A = B ) -> Pred ( R , A , y ) = Pred ( S , B , y ) )
6 5 3adant3 
 |-  ( ( R = S /\ A = B /\ F = G ) -> Pred ( R , A , y ) = Pred ( S , B , y ) )
7 6 sseq1d 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( Pred ( R , A , y ) C_ x <-> Pred ( S , B , y ) C_ x ) )
8 7 ralbidv 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( A. y e. x Pred ( R , A , y ) C_ x <-> A. y e. x Pred ( S , B , y ) C_ x ) )
9 2 8 anbi12d 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) <-> ( x C_ B /\ A. y e. x Pred ( S , B , y ) C_ x ) ) )
10 simp3 
 |-  ( ( R = S /\ A = B /\ F = G ) -> F = G )
11 5 reseq2d 
 |-  ( ( R = S /\ A = B ) -> ( f |` Pred ( R , A , y ) ) = ( f |` Pred ( S , B , y ) ) )
12 11 3adant3 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( f |` Pred ( R , A , y ) ) = ( f |` Pred ( S , B , y ) ) )
13 10 12 fveq12d 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( F ` ( f |` Pred ( R , A , y ) ) ) = ( G ` ( f |` Pred ( S , B , y ) ) ) )
14 13 eqeq2d 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) <-> ( f ` y ) = ( G ` ( f |` Pred ( S , B , y ) ) ) ) )
15 14 ralbidv 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) <-> A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( S , B , y ) ) ) ) )
16 9 15 3anbi23d 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) <-> ( f Fn x /\ ( x C_ B /\ A. y e. x Pred ( S , B , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( S , B , y ) ) ) ) ) )
17 16 exbidv 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) <-> E. x ( f Fn x /\ ( x C_ B /\ A. y e. x Pred ( S , B , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( S , B , y ) ) ) ) ) )
18 17 abbidv 
 |-  ( ( R = S /\ A = B /\ F = G ) -> { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) } = { f | E. x ( f Fn x /\ ( x C_ B /\ A. y e. x Pred ( S , B , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( S , B , y ) ) ) ) } )
19 18 unieqd 
 |-  ( ( R = S /\ A = B /\ F = G ) -> U. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) } = U. { f | E. x ( f Fn x /\ ( x C_ B /\ A. y e. x Pred ( S , B , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( S , B , y ) ) ) ) } )
20 df-wrecs 
 |-  wrecs ( R , A , F ) = U. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( F ` ( f |` Pred ( R , A , y ) ) ) ) }
21 df-wrecs 
 |-  wrecs ( S , B , G ) = U. { f | E. x ( f Fn x /\ ( x C_ B /\ A. y e. x Pred ( S , B , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( S , B , y ) ) ) ) }
22 19 20 21 3eqtr4g 
 |-  ( ( R = S /\ A = B /\ F = G ) -> wrecs ( R , A , F ) = wrecs ( S , B , G ) )