Metamath Proof Explorer


Theorem satf0suc

Description: The value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation at a successor. (Contributed by AV, 19-Sep-2023)

Ref Expression
Hypothesis satf0suc.s S = Sat
Assertion satf0suc N ω S suc N = S N x y | y = u S N v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u

Proof

Step Hyp Ref Expression
1 satf0suc.s S = Sat
2 1 fveq1i S suc N = Sat suc N
3 2 a1i N ω S suc N = Sat suc N
4 omsucelsucb N ω suc N suc ω
5 satf0sucom suc N suc ω Sat suc N = rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j suc N
6 4 5 sylbi N ω Sat suc N = rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j suc N
7 nnon N ω N On
8 rdgsuc N On rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j suc N = f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N
9 7 8 syl N ω rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j suc N = f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N
10 elelsuc N ω N suc ω
11 satf0sucom N suc ω Sat N = rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N
12 10 11 syl N ω Sat N = rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N
13 1 eqcomi Sat = S
14 13 fveq1i Sat N = S N
15 12 14 eqtr3di N ω rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N = S N
16 15 fveq2d N ω f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j N = f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u S N
17 eqidd N ω f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
18 id f = S N f = S N
19 rexeq f = S N v f x = 1 st u 𝑔 1 st v v S N x = 1 st u 𝑔 1 st v
20 19 orbi1d f = S N v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
21 20 rexeqbi1dv f = S N u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u u S N v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
22 21 anbi2d f = S N y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u y = u S N v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
23 22 opabbidv f = S N x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = x y | y = u S N v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
24 18 23 uneq12d f = S N f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = S N x y | y = u S N v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
25 24 adantl N ω f = S N f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = S N x y | y = u S N v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
26 fvex S N V
27 26 a1i N ω S N V
28 omex ω V
29 satf0suclem S N V S N V ω V x y | y = u S N v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
30 26 26 28 29 mp3an x y | y = u S N v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
31 26 30 unex S N x y | y = u S N v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
32 31 a1i N ω S N x y | y = u S N v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u V
33 17 25 27 32 fvmptd N ω f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u S N = S N x y | y = u S N v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
34 9 16 33 3eqtrd N ω rec f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x y | y = i ω j ω x = i 𝑔 j suc N = S N x y | y = u S N v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
35 3 6 34 3eqtrd N ω S suc N = S N x y | y = u S N v S N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u