Step |
Hyp |
Ref |
Expression |
1 |
|
satfv0fv.s |
|- S = ( M Sat E ) |
2 |
|
satfv0fun |
|- ( ( M e. V /\ E e. W ) -> Fun ( ( M Sat E ) ` (/) ) ) |
3 |
1
|
fveq1i |
|- ( S ` (/) ) = ( ( M Sat E ) ` (/) ) |
4 |
3
|
funeqi |
|- ( Fun ( S ` (/) ) <-> Fun ( ( M Sat E ) ` (/) ) ) |
5 |
2 4
|
sylibr |
|- ( ( M e. V /\ E e. W ) -> Fun ( S ` (/) ) ) |
6 |
5
|
3adant3 |
|- ( ( M e. V /\ E e. W /\ X e. ( Fmla ` (/) ) ) -> Fun ( S ` (/) ) ) |
7 |
|
fmla0 |
|- ( Fmla ` (/) ) = { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) } |
8 |
7
|
eleq2i |
|- ( X e. ( Fmla ` (/) ) <-> X e. { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) } ) |
9 |
|
eqeq1 |
|- ( x = X -> ( x = ( i e.g j ) <-> X = ( i e.g j ) ) ) |
10 |
9
|
2rexbidv |
|- ( x = X -> ( E. i e. _om E. j e. _om x = ( i e.g j ) <-> E. i e. _om E. j e. _om X = ( i e.g j ) ) ) |
11 |
10
|
elrab |
|- ( X e. { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) } <-> ( X e. _V /\ E. i e. _om E. j e. _om X = ( i e.g j ) ) ) |
12 |
8 11
|
bitri |
|- ( X e. ( Fmla ` (/) ) <-> ( X e. _V /\ E. i e. _om E. j e. _om X = ( i e.g j ) ) ) |
13 |
|
simpr |
|- ( ( ( i e. _om /\ j e. _om ) /\ X = ( i e.g j ) ) -> X = ( i e.g j ) ) |
14 |
|
goel |
|- ( ( i e. _om /\ j e. _om ) -> ( i e.g j ) = <. (/) , <. i , j >. >. ) |
15 |
14
|
eqeq2d |
|- ( ( i e. _om /\ j e. _om ) -> ( X = ( i e.g j ) <-> X = <. (/) , <. i , j >. >. ) ) |
16 |
|
2fveq3 |
|- ( X = <. (/) , <. i , j >. >. -> ( 1st ` ( 2nd ` X ) ) = ( 1st ` ( 2nd ` <. (/) , <. i , j >. >. ) ) ) |
17 |
|
0ex |
|- (/) e. _V |
18 |
|
opex |
|- <. i , j >. e. _V |
19 |
17 18
|
op2nd |
|- ( 2nd ` <. (/) , <. i , j >. >. ) = <. i , j >. |
20 |
19
|
fveq2i |
|- ( 1st ` ( 2nd ` <. (/) , <. i , j >. >. ) ) = ( 1st ` <. i , j >. ) |
21 |
|
vex |
|- i e. _V |
22 |
|
vex |
|- j e. _V |
23 |
21 22
|
op1st |
|- ( 1st ` <. i , j >. ) = i |
24 |
20 23
|
eqtri |
|- ( 1st ` ( 2nd ` <. (/) , <. i , j >. >. ) ) = i |
25 |
16 24
|
eqtrdi |
|- ( X = <. (/) , <. i , j >. >. -> ( 1st ` ( 2nd ` X ) ) = i ) |
26 |
25
|
fveq2d |
|- ( X = <. (/) , <. i , j >. >. -> ( a ` ( 1st ` ( 2nd ` X ) ) ) = ( a ` i ) ) |
27 |
|
2fveq3 |
|- ( X = <. (/) , <. i , j >. >. -> ( 2nd ` ( 2nd ` X ) ) = ( 2nd ` ( 2nd ` <. (/) , <. i , j >. >. ) ) ) |
28 |
19
|
fveq2i |
|- ( 2nd ` ( 2nd ` <. (/) , <. i , j >. >. ) ) = ( 2nd ` <. i , j >. ) |
29 |
21 22
|
op2nd |
|- ( 2nd ` <. i , j >. ) = j |
30 |
28 29
|
eqtri |
|- ( 2nd ` ( 2nd ` <. (/) , <. i , j >. >. ) ) = j |
31 |
27 30
|
eqtrdi |
|- ( X = <. (/) , <. i , j >. >. -> ( 2nd ` ( 2nd ` X ) ) = j ) |
32 |
31
|
fveq2d |
|- ( X = <. (/) , <. i , j >. >. -> ( a ` ( 2nd ` ( 2nd ` X ) ) ) = ( a ` j ) ) |
33 |
26 32
|
breq12d |
|- ( X = <. (/) , <. i , j >. >. -> ( ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) <-> ( a ` i ) E ( a ` j ) ) ) |
34 |
15 33
|
syl6bi |
|- ( ( i e. _om /\ j e. _om ) -> ( X = ( i e.g j ) -> ( ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) <-> ( a ` i ) E ( a ` j ) ) ) ) |
35 |
34
|
imp |
|- ( ( ( i e. _om /\ j e. _om ) /\ X = ( i e.g j ) ) -> ( ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) <-> ( a ` i ) E ( a ` j ) ) ) |
36 |
35
|
rabbidv |
|- ( ( ( i e. _om /\ j e. _om ) /\ X = ( i e.g j ) ) -> { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) |
37 |
13 36
|
jca |
|- ( ( ( i e. _om /\ j e. _om ) /\ X = ( i e.g j ) ) -> ( X = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) |
38 |
37
|
ex |
|- ( ( i e. _om /\ j e. _om ) -> ( X = ( i e.g j ) -> ( X = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) ) |
39 |
38
|
reximdva |
|- ( i e. _om -> ( E. j e. _om X = ( i e.g j ) -> E. j e. _om ( X = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) ) |
40 |
39
|
reximia |
|- ( E. i e. _om E. j e. _om X = ( i e.g j ) -> E. i e. _om E. j e. _om ( X = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) |
41 |
12 40
|
simplbiim |
|- ( X e. ( Fmla ` (/) ) -> E. i e. _om E. j e. _om ( X = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) |
42 |
41
|
3ad2ant3 |
|- ( ( M e. V /\ E e. W /\ X e. ( Fmla ` (/) ) ) -> E. i e. _om E. j e. _om ( X = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) |
43 |
|
simp3 |
|- ( ( M e. V /\ E e. W /\ X e. ( Fmla ` (/) ) ) -> X e. ( Fmla ` (/) ) ) |
44 |
|
ovex |
|- ( M ^m _om ) e. _V |
45 |
44
|
rabex |
|- { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } e. _V |
46 |
|
eqeq1 |
|- ( y = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } -> ( y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } <-> { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) |
47 |
9 46
|
bi2anan9 |
|- ( ( x = X /\ y = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } ) -> ( ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) <-> ( X = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) ) |
48 |
47
|
2rexbidv |
|- ( ( x = X /\ y = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } ) -> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) <-> E. i e. _om E. j e. _om ( X = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) ) |
49 |
48
|
opelopabga |
|- ( ( X e. ( Fmla ` (/) ) /\ { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } e. _V ) -> ( <. X , { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } >. e. { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) } <-> E. i e. _om E. j e. _om ( X = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) ) |
50 |
43 45 49
|
sylancl |
|- ( ( M e. V /\ E e. W /\ X e. ( Fmla ` (/) ) ) -> ( <. X , { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } >. e. { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) } <-> E. i e. _om E. j e. _om ( X = ( i e.g j ) /\ { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) ) ) |
51 |
42 50
|
mpbird |
|- ( ( M e. V /\ E e. W /\ X e. ( Fmla ` (/) ) ) -> <. X , { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } >. e. { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) } ) |
52 |
1
|
satfv0 |
|- ( ( M e. V /\ E e. W ) -> ( S ` (/) ) = { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) } ) |
53 |
52
|
eleq2d |
|- ( ( M e. V /\ E e. W ) -> ( <. X , { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } >. e. ( S ` (/) ) <-> <. X , { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } >. e. { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) } ) ) |
54 |
53
|
3adant3 |
|- ( ( M e. V /\ E e. W /\ X e. ( Fmla ` (/) ) ) -> ( <. X , { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } >. e. ( S ` (/) ) <-> <. X , { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } >. e. { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { a e. ( M ^m _om ) | ( a ` i ) E ( a ` j ) } ) } ) ) |
55 |
51 54
|
mpbird |
|- ( ( M e. V /\ E e. W /\ X e. ( Fmla ` (/) ) ) -> <. X , { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } >. e. ( S ` (/) ) ) |
56 |
|
funopfv |
|- ( Fun ( S ` (/) ) -> ( <. X , { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } >. e. ( S ` (/) ) -> ( ( S ` (/) ) ` X ) = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } ) ) |
57 |
6 55 56
|
sylc |
|- ( ( M e. V /\ E e. W /\ X e. ( Fmla ` (/) ) ) -> ( ( S ` (/) ) ` X ) = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) E ( a ` ( 2nd ` ( 2nd ` X ) ) ) } ) |