Metamath Proof Explorer


Theorem satf0

Description: The satisfaction predicate as function over wff codes in the empty model with an empty binary relation. (Contributed by AV, 14-Sep-2023)

Ref Expression
Assertion satf0 Sat = 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 ω

Proof

Step Hyp Ref Expression
1 0ex V
2 satf V V Sat = rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a ω | a i a j suc ω
3 1 1 2 mp2an Sat = rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a ω | a i a j suc ω
4 peano1 ω
5 4 ne0ii ω
6 map0b ω ω =
7 5 6 ax-mp ω =
8 7 difeq1i ω 2 nd u 2 nd v = 2 nd u 2 nd v
9 0dif 2 nd u 2 nd v =
10 8 9 eqtri ω 2 nd u 2 nd v =
11 10 eqeq2i y = ω 2 nd u 2 nd v y =
12 11 anbi2i x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v x = 1 st u 𝑔 1 st v y =
13 12 rexbii v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v v f x = 1 st u 𝑔 1 st v y =
14 r19.41v v f x = 1 st u 𝑔 1 st v y = v f x = 1 st u 𝑔 1 st v y =
15 13 14 bitri v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v v f x = 1 st u 𝑔 1 st v y =
16 7 rabeqi a ω | z i z a ω i 2 nd u = a | z i z a ω i 2 nd u
17 rab0 a | z i z a ω i 2 nd u =
18 16 17 eqtri a ω | z i z a ω i 2 nd u =
19 18 eqeq2i y = a ω | z i z a ω i 2 nd u y =
20 19 anbi2i x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u x = 𝑔 i 1 st u y =
21 20 rexbii i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u i ω x = 𝑔 i 1 st u y =
22 r19.41v i ω x = 𝑔 i 1 st u y = i ω x = 𝑔 i 1 st u y =
23 21 22 bitri i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u i ω x = 𝑔 i 1 st u y =
24 15 23 orbi12i v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u v f x = 1 st u 𝑔 1 st v y = i ω x = 𝑔 i 1 st u y =
25 24 rexbii u f v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u u f v f x = 1 st u 𝑔 1 st v y = i ω x = 𝑔 i 1 st u y =
26 andir v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u y = v f x = 1 st u 𝑔 1 st v y = i ω x = 𝑔 i 1 st u y =
27 26 bicomi v f x = 1 st u 𝑔 1 st v y = i ω x = 𝑔 i 1 st u y = v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u y =
28 27 rexbii u f v f x = 1 st u 𝑔 1 st v y = i ω x = 𝑔 i 1 st u y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u y =
29 r19.41v u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u y =
30 25 28 29 3bitri u f v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u y =
31 30 biancomi u f v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
32 31 opabbii x y | u f v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u = x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
33 32 uneq2i f x y | u f v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u = f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
34 33 mpteq2i f V f x y | u f v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u = f V f x y | y = u f v f x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
35 7 rabeqi a ω | a i a j = a | a i a j
36 rab0 a | a i a j =
37 35 36 eqtri a ω | a i a j =
38 37 eqeq2i y = a ω | a i a j y =
39 38 anbi2i x = i 𝑔 j y = a ω | a i a j x = i 𝑔 j y =
40 39 2rexbii i ω j ω x = i 𝑔 j y = a ω | a i a j i ω j ω x = i 𝑔 j y =
41 r19.41vv i ω j ω x = i 𝑔 j y = i ω j ω x = i 𝑔 j y =
42 40 41 bitri i ω j ω x = i 𝑔 j y = a ω | a i a j i ω j ω x = i 𝑔 j y =
43 42 biancomi i ω j ω x = i 𝑔 j y = a ω | a i a j y = i ω j ω x = i 𝑔 j
44 43 opabbii x y | i ω j ω x = i 𝑔 j y = a ω | a i a j = x y | y = i ω j ω x = i 𝑔 j
45 rdgeq12 f V f x y | u f v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u = 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 | i ω j ω x = i 𝑔 j y = a ω | a i a j = x y | y = i ω j ω x = i 𝑔 j rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a ω | a i a j = 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
46 34 44 45 mp2an rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a ω | a i a j = 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
47 46 reseq1i rec f V f x y | u f v f x = 1 st u 𝑔 1 st v y = ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a ω | z i z a ω i 2 nd u x y | i ω j ω x = i 𝑔 j y = a ω | a i a j suc ω = 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 ω
48 3 47 eqtri Sat = 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 ω