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 V E W X Fmla S X = a M ω | a 1 st 2 nd X E a 2 nd 2 nd X

Proof

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