Metamath Proof Explorer


Theorem satfrel

Description: The value of the satisfaction predicate as function over wff codes at a natural number is a relation. (Contributed by AV, 12-Oct-2023)

Ref Expression
Assertion satfrel M V E W N ω Rel M Sat E N

Proof

Step Hyp Ref Expression
1 fveq2 a = M Sat E a = M Sat E
2 1 releqd a = Rel M Sat E a Rel M Sat E
3 2 imbi2d a = M V E W Rel M Sat E a M V E W Rel M Sat E
4 fveq2 a = b M Sat E a = M Sat E b
5 4 releqd a = b Rel M Sat E a Rel M Sat E b
6 5 imbi2d a = b M V E W Rel M Sat E a M V E W Rel M Sat E b
7 fveq2 a = suc b M Sat E a = M Sat E suc b
8 7 releqd a = suc b Rel M Sat E a Rel M Sat E suc b
9 8 imbi2d a = suc b M V E W Rel M Sat E a M V E W Rel M Sat E suc b
10 fveq2 a = N M Sat E a = M Sat E N
11 10 releqd a = N Rel M Sat E a Rel M Sat E N
12 11 imbi2d a = N M V E W Rel M Sat E a M V E W Rel M Sat E N
13 relopabv Rel x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j
14 eqid M Sat E = M Sat E
15 14 satfv0 M V E W M Sat E = x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j
16 15 releqd M V E W Rel M Sat E Rel x y | i ω j ω x = i 𝑔 j y = a M ω | a i E a j
17 13 16 mpbiri M V E W Rel M Sat E
18 pm2.27 M V E W M V E W Rel M Sat E b Rel M Sat E b
19 simpr M V E W b ω Rel M Sat E b Rel M Sat E b
20 relopabv Rel x y | u M Sat E b v M Sat E b 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
21 relun Rel M Sat E b x y | u M Sat E b v M Sat E b 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 Rel M Sat E b Rel x y | u M Sat E b v M Sat E b 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
22 19 20 21 sylanblrc M V E W b ω Rel M Sat E b Rel M Sat E b x y | u M Sat E b v M Sat E b 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
23 14 satfvsuc M V E W b ω M Sat E suc b = M Sat E b x y | u M Sat E b v M Sat E b 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
24 23 ad4ant123 M V E W b ω Rel M Sat E b M Sat E suc b = M Sat E b x y | u M Sat E b v M Sat E b 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
25 24 releqd M V E W b ω Rel M Sat E b Rel M Sat E suc b Rel M Sat E b x y | u M Sat E b v M Sat E b 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
26 22 25 mpbird M V E W b ω Rel M Sat E b Rel M Sat E suc b
27 26 exp31 M V E W b ω Rel M Sat E b Rel M Sat E suc b
28 27 com23 M V E W Rel M Sat E b b ω Rel M Sat E suc b
29 18 28 syld M V E W M V E W Rel M Sat E b b ω Rel M Sat E suc b
30 29 com13 b ω M V E W Rel M Sat E b M V E W Rel M Sat E suc b
31 3 6 9 12 17 30 finds N ω M V E W Rel M Sat E N
32 31 com12 M V E W N ω Rel M Sat E N
33 32 3impia M V E W N ω Rel M Sat E N