Metamath Proof Explorer


Theorem satfv0

Description: The value of the satisfaction predicate as function over wff codes at (/) . (Contributed by AV, 8-Oct-2023)

Ref Expression
Hypothesis satfv0.s S = M Sat E
Assertion satfv0 M V E W S = x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j

Proof

Step Hyp Ref Expression
1 satfv0.s S = M Sat E
2 peano1 ω
3 elelsuc ω suc ω
4 2 3 mp1i M V E W suc ω
5 1 satfvsucom M V E W suc ω S = rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j
6 4 5 mpd3an3 M V E W S = rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j
7 goelel3xp i ω j ω i 𝑔 j ω × ω × ω
8 eleq1 x = i 𝑔 j x ω × ω × ω i 𝑔 j ω × ω × ω
9 7 8 syl5ibrcom i ω j ω x = i 𝑔 j x ω × ω × ω
10 9 adantrd i ω j ω x = i 𝑔 j y = a M ω | a i E a j x ω × ω × ω
11 10 pm4.71d i ω j ω x = i 𝑔 j y = a M ω | a i E a j x = i 𝑔 j y = a M ω | a i E a j x ω × ω × ω
12 11 2rexbiia i ω j ω x = i 𝑔 j y = a M ω | a i E a j i ω j ω x = i 𝑔 j y = a M ω | a i E a j x ω × ω × ω
13 r19.41vv i ω j ω x = i 𝑔 j y = a M ω | a i E a j x ω × ω × ω i ω j ω x = i 𝑔 j y = a M ω | a i E a j x ω × ω × ω
14 ancom i ω j ω x = i 𝑔 j y = a M ω | a i E a j x ω × ω × ω x ω × ω × ω i ω j ω x = i 𝑔 j y = a M ω | a i E a j
15 12 13 14 3bitri i ω j ω x = i 𝑔 j y = a M ω | a i E a j x ω × ω × ω i ω j ω x = i 𝑔 j y = a M ω | a i E a j
16 15 opabbii x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j = x y | x ω × ω × ω i ω j ω x = i 𝑔 j y = a M ω | a i E a j
17 omex ω V
18 17 17 xpex ω × ω V
19 xpexg ω V ω × ω V ω × ω × ω V
20 oveq1 i = m i 𝑔 j = m 𝑔 j
21 20 eqeq2d i = m x = i 𝑔 j x = m 𝑔 j
22 fveq2 i = m a i = a m
23 22 breq1d i = m a i E a j a m E a j
24 23 rabbidv i = m a M ω | a i E a j = a M ω | a m E a j
25 24 eqeq2d i = m y = a M ω | a i E a j y = a M ω | a m E a j
26 21 25 anbi12d i = m x = i 𝑔 j y = a M ω | a i E a j x = m 𝑔 j y = a M ω | a m E a j
27 oveq2 j = n m 𝑔 j = m 𝑔 n
28 27 eqeq2d j = n x = m 𝑔 j x = m 𝑔 n
29 fveq2 j = n a j = a n
30 29 breq2d j = n a m E a j a m E a n
31 30 rabbidv j = n a M ω | a m E a j = a M ω | a m E a n
32 31 eqeq2d j = n y = a M ω | a m E a j y = a M ω | a m E a n
33 28 32 anbi12d j = n x = m 𝑔 j y = a M ω | a m E a j x = m 𝑔 n y = a M ω | a m E a n
34 26 33 cbvrex2vw i ω j ω x = i 𝑔 j y = a M ω | a i E a j m ω n ω x = m 𝑔 n y = a M ω | a m E a n
35 eqeq1 x = i 𝑔 j x = m 𝑔 n i 𝑔 j = m 𝑔 n
36 35 adantl m ω n ω i ω j ω x = i 𝑔 j x = m 𝑔 n i 𝑔 j = m 𝑔 n
37 goeleq12bg m ω n ω i ω j ω i 𝑔 j = m 𝑔 n i = m j = n
38 22 eqcomd i = m a m = a i
39 29 eqcomd j = n a n = a j
40 38 39 breqan12d i = m j = n a m E a n a i E a j
41 40 rabbidv i = m j = n a M ω | a m E a n = a M ω | a i E a j
42 37 41 syl6bi m ω n ω i ω j ω i 𝑔 j = m 𝑔 n a M ω | a m E a n = a M ω | a i E a j
43 42 imp m ω n ω i ω j ω i 𝑔 j = m 𝑔 n a M ω | a m E a n = a M ω | a i E a j
44 eqeq12 y = a M ω | a m E a n z = a M ω | a i E a j y = z a M ω | a m E a n = a M ω | a i E a j
45 43 44 syl5ibrcom m ω n ω i ω j ω i 𝑔 j = m 𝑔 n y = a M ω | a m E a n z = a M ω | a i E a j y = z
46 45 exp4b m ω n ω i ω j ω i 𝑔 j = m 𝑔 n y = a M ω | a m E a n z = a M ω | a i E a j y = z
47 46 adantr m ω n ω i ω j ω x = i 𝑔 j i 𝑔 j = m 𝑔 n y = a M ω | a m E a n z = a M ω | a i E a j y = z
48 36 47 sylbid m ω n ω i ω j ω x = i 𝑔 j x = m 𝑔 n y = a M ω | a m E a n z = a M ω | a i E a j y = z
49 48 impd m ω n ω i ω j ω x = i 𝑔 j x = m 𝑔 n y = a M ω | a m E a n z = a M ω | a i E a j y = z
50 49 com23 m ω n ω i ω j ω x = i 𝑔 j z = a M ω | a i E a j x = m 𝑔 n y = a M ω | a m E a n y = z
51 50 expimpd m ω n ω i ω j ω x = i 𝑔 j z = a M ω | a i E a j x = m 𝑔 n y = a M ω | a m E a n y = z
52 51 rexlimdvva m ω n ω i ω j ω x = i 𝑔 j z = a M ω | a i E a j x = m 𝑔 n y = a M ω | a m E a n y = z
53 52 com23 m ω n ω x = m 𝑔 n y = a M ω | a m E a n i ω j ω x = i 𝑔 j z = a M ω | a i E a j y = z
54 53 rexlimivv m ω n ω x = m 𝑔 n y = a M ω | a m E a n i ω j ω x = i 𝑔 j z = a M ω | a i E a j y = z
55 34 54 sylbi i ω j ω x = i 𝑔 j y = a M ω | a i E a j i ω j ω x = i 𝑔 j z = a M ω | a i E a j y = z
56 55 imp i ω j ω x = i 𝑔 j y = a M ω | a i E a j i ω j ω x = i 𝑔 j z = a M ω | a i E a j y = z
57 56 gen2 y z i ω j ω x = i 𝑔 j y = a M ω | a i E a j i ω j ω x = i 𝑔 j z = a M ω | a i E a j y = z
58 eqeq1 y = z y = a M ω | a i E a j z = a M ω | a i E a j
59 58 anbi2d y = z x = i 𝑔 j y = a M ω | a i E a j x = i 𝑔 j z = a M ω | a i E a j
60 59 2rexbidv y = z i ω j ω x = i 𝑔 j y = a M ω | a i E a j i ω j ω x = i 𝑔 j z = a M ω | a i E a j
61 60 mo4 * y i ω j ω x = i 𝑔 j y = a M ω | a i E a j y z i ω j ω x = i 𝑔 j y = a M ω | a i E a j i ω j ω x = i 𝑔 j z = a M ω | a i E a j y = z
62 57 61 mpbir * y i ω j ω x = i 𝑔 j y = a M ω | a i E a j
63 moabex * y i ω j ω x = i 𝑔 j y = a M ω | a i E a j y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j V
64 62 63 mp1i ω V ω × ω V x ω × ω × ω y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j V
65 19 64 opabex3d ω V ω × ω V x y | x ω × ω × ω i ω j ω x = i 𝑔 j y = a M ω | a i E a j V
66 17 18 65 mp2an x y | x ω × ω × ω i ω j ω x = i 𝑔 j y = a M ω | a i E a j V
67 16 66 eqeltri x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j V
68 67 rdg0 rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j = x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j
69 6 68 eqtrdi M V E W S = x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j