Step |
Hyp |
Ref |
Expression |
1 |
|
shftfval.1 |
|- F e. _V |
2 |
|
ovex |
|- ( x - A ) e. _V |
3 |
|
vex |
|- y e. _V |
4 |
2 3
|
breldm |
|- ( ( x - A ) F y -> ( x - A ) e. dom F ) |
5 |
|
npcan |
|- ( ( x e. CC /\ A e. CC ) -> ( ( x - A ) + A ) = x ) |
6 |
5
|
eqcomd |
|- ( ( x e. CC /\ A e. CC ) -> x = ( ( x - A ) + A ) ) |
7 |
6
|
ancoms |
|- ( ( A e. CC /\ x e. CC ) -> x = ( ( x - A ) + A ) ) |
8 |
|
oveq1 |
|- ( w = ( x - A ) -> ( w + A ) = ( ( x - A ) + A ) ) |
9 |
8
|
rspceeqv |
|- ( ( ( x - A ) e. dom F /\ x = ( ( x - A ) + A ) ) -> E. w e. dom F x = ( w + A ) ) |
10 |
4 7 9
|
syl2anr |
|- ( ( ( A e. CC /\ x e. CC ) /\ ( x - A ) F y ) -> E. w e. dom F x = ( w + A ) ) |
11 |
|
vex |
|- x e. _V |
12 |
|
eqeq1 |
|- ( z = x -> ( z = ( w + A ) <-> x = ( w + A ) ) ) |
13 |
12
|
rexbidv |
|- ( z = x -> ( E. w e. dom F z = ( w + A ) <-> E. w e. dom F x = ( w + A ) ) ) |
14 |
11 13
|
elab |
|- ( x e. { z | E. w e. dom F z = ( w + A ) } <-> E. w e. dom F x = ( w + A ) ) |
15 |
10 14
|
sylibr |
|- ( ( ( A e. CC /\ x e. CC ) /\ ( x - A ) F y ) -> x e. { z | E. w e. dom F z = ( w + A ) } ) |
16 |
2 3
|
brelrn |
|- ( ( x - A ) F y -> y e. ran F ) |
17 |
16
|
adantl |
|- ( ( ( A e. CC /\ x e. CC ) /\ ( x - A ) F y ) -> y e. ran F ) |
18 |
15 17
|
jca |
|- ( ( ( A e. CC /\ x e. CC ) /\ ( x - A ) F y ) -> ( x e. { z | E. w e. dom F z = ( w + A ) } /\ y e. ran F ) ) |
19 |
18
|
expl |
|- ( A e. CC -> ( ( x e. CC /\ ( x - A ) F y ) -> ( x e. { z | E. w e. dom F z = ( w + A ) } /\ y e. ran F ) ) ) |
20 |
19
|
ssopab2dv |
|- ( A e. CC -> { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } C_ { <. x , y >. | ( x e. { z | E. w e. dom F z = ( w + A ) } /\ y e. ran F ) } ) |
21 |
|
df-xp |
|- ( { z | E. w e. dom F z = ( w + A ) } X. ran F ) = { <. x , y >. | ( x e. { z | E. w e. dom F z = ( w + A ) } /\ y e. ran F ) } |
22 |
20 21
|
sseqtrrdi |
|- ( A e. CC -> { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } C_ ( { z | E. w e. dom F z = ( w + A ) } X. ran F ) ) |
23 |
1
|
dmex |
|- dom F e. _V |
24 |
23
|
abrexex |
|- { z | E. w e. dom F z = ( w + A ) } e. _V |
25 |
1
|
rnex |
|- ran F e. _V |
26 |
24 25
|
xpex |
|- ( { z | E. w e. dom F z = ( w + A ) } X. ran F ) e. _V |
27 |
|
ssexg |
|- ( ( { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } C_ ( { z | E. w e. dom F z = ( w + A ) } X. ran F ) /\ ( { z | E. w e. dom F z = ( w + A ) } X. ran F ) e. _V ) -> { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } e. _V ) |
28 |
22 26 27
|
sylancl |
|- ( A e. CC -> { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } e. _V ) |
29 |
|
breq |
|- ( z = F -> ( ( x - w ) z y <-> ( x - w ) F y ) ) |
30 |
29
|
anbi2d |
|- ( z = F -> ( ( x e. CC /\ ( x - w ) z y ) <-> ( x e. CC /\ ( x - w ) F y ) ) ) |
31 |
30
|
opabbidv |
|- ( z = F -> { <. x , y >. | ( x e. CC /\ ( x - w ) z y ) } = { <. x , y >. | ( x e. CC /\ ( x - w ) F y ) } ) |
32 |
|
oveq2 |
|- ( w = A -> ( x - w ) = ( x - A ) ) |
33 |
32
|
breq1d |
|- ( w = A -> ( ( x - w ) F y <-> ( x - A ) F y ) ) |
34 |
33
|
anbi2d |
|- ( w = A -> ( ( x e. CC /\ ( x - w ) F y ) <-> ( x e. CC /\ ( x - A ) F y ) ) ) |
35 |
34
|
opabbidv |
|- ( w = A -> { <. x , y >. | ( x e. CC /\ ( x - w ) F y ) } = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } ) |
36 |
|
df-shft |
|- shift = ( z e. _V , w e. CC |-> { <. x , y >. | ( x e. CC /\ ( x - w ) z y ) } ) |
37 |
31 35 36
|
ovmpog |
|- ( ( F e. _V /\ A e. CC /\ { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } e. _V ) -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } ) |
38 |
1 37
|
mp3an1 |
|- ( ( A e. CC /\ { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } e. _V ) -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } ) |
39 |
28 38
|
mpdan |
|- ( A e. CC -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } ) |