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 ) )