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