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