Metamath Proof Explorer

Theorem satfv0fvfmla0

Description: The value of the satisfaction predicate as function over a wff code at (/) . (Contributed by AV, 2-Nov-2023)

Ref Expression
Hypothesis satfv0fv.s 
|- S = ( M Sat E )
Assertion satfv0fvfmla0 
|- ( ( 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 ) ) ) } )

Proof

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 biimtrdi 
 |-  ( ( 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 ) ) ) } )