Metamath Proof Explorer

Theorem frecseq123

Description: Equality theorem for the well-founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( R = S /\ A = B /\ F = G ) -> A = B )
2 1 sseq2d 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( x C_ A <-> x C_ B ) )
3 equid 
 |-  y = y
4 predeq123 
 |-  ( ( R = S /\ A = B /\ y = y ) -> Pred ( R , A , y ) = Pred ( S , B , y ) )
5 3 4 mp3an3 
 |-  ( ( 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 10 oveqd 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( y F ( f |` Pred ( R , A , y ) ) ) = ( y G ( f |` Pred ( R , A , y ) ) ) )
12 6 reseq2d 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( f |` Pred ( R , A , y ) ) = ( f |` Pred ( S , B , y ) ) )
13 12 oveq2d 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( y G ( f |` Pred ( R , A , y ) ) ) = ( y G ( f |` Pred ( S , B , y ) ) ) )
14 11 13 eqtrd 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( y F ( f |` Pred ( R , A , y ) ) ) = ( y G ( f |` Pred ( S , B , y ) ) ) )
15 14 eqeq2d 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( ( f ` y ) = ( y F ( f |` Pred ( R , A , y ) ) ) <-> ( f ` y ) = ( y G ( f |` Pred ( S , B , y ) ) ) ) )
16 15 ralbidv 
 |-  ( ( R = S /\ A = B /\ F = G ) -> ( A. y e. x ( f ` y ) = ( y F ( f |` Pred ( R , A , y ) ) ) <-> A. y e. x ( f ` y ) = ( y G ( f |` Pred ( S , B , y ) ) ) ) )
17 9 16 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 ) = ( 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 ) = ( y G ( f |` Pred ( S , B , y ) ) ) ) ) )
18 17 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 ) = ( 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 ) = ( y G ( f |` Pred ( S , B , y ) ) ) ) ) )
19 18 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 ) = ( 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 ) = ( y G ( f |` Pred ( S , B , y ) ) ) ) } )
20 19 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 ) = ( 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 ) = ( y G ( f |` Pred ( S , B , y ) ) ) ) } )
21 df-frecs 
 |-  frecs ( 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 ) = ( y F ( f |` Pred ( R , A , y ) ) ) ) }
22 df-frecs 
 |-  frecs ( 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 ) = ( y G ( f |` Pred ( S , B , y ) ) ) ) }
23 20 21 22 3eqtr4g 
 |-  ( ( R = S /\ A = B /\ F = G ) -> frecs ( R , A , F ) = frecs ( S , B , G ) )