Metamath Proof Explorer


Theorem satf0op

Description: An element of a value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation expressed as ordered pair. (Contributed by AV, 19-Sep-2023)

Ref Expression
Hypothesis satf0op.s S = Sat
Assertion satf0op N ω X S N x X = x x S N

Proof

Step Hyp Ref Expression
1 satf0op.s S = Sat
2 fveq2 y = S y = S
3 2 eleq2d y = X S y X S
4 2 eleq2d y = x S y x S
5 4 anbi2d y = X = x x S y X = x x S
6 5 exbidv y = x X = x x S y x X = x x S
7 3 6 bibi12d y = X S y x X = x x S y X S x X = x x S
8 fveq2 y = z S y = S z
9 8 eleq2d y = z X S y X S z
10 8 eleq2d y = z x S y x S z
11 10 anbi2d y = z X = x x S y X = x x S z
12 11 exbidv y = z x X = x x S y x X = x x S z
13 9 12 bibi12d y = z X S y x X = x x S y X S z x X = x x S z
14 fveq2 y = suc z S y = S suc z
15 14 eleq2d y = suc z X S y X S suc z
16 14 eleq2d y = suc z x S y x S suc z
17 16 anbi2d y = suc z X = x x S y X = x x S suc z
18 17 exbidv y = suc z x X = x x S y x X = x x S suc z
19 15 18 bibi12d y = suc z X S y x X = x x S y X S suc z x X = x x S suc z
20 fveq2 y = N S y = S N
21 20 eleq2d y = N X S y X S N
22 20 eleq2d y = N x S y x S N
23 22 anbi2d y = N X = x x S y X = x x S N
24 23 exbidv y = N x X = x x S y x X = x x S N
25 21 24 bibi12d y = N X S y x X = x x S y X S N x X = x x S N
26 1 fveq1i S = Sat
27 satf00 Sat = x y | y = i ω j ω x = i 𝑔 j
28 26 27 eqtri S = x y | y = i ω j ω x = i 𝑔 j
29 28 eleq2i X S X x y | y = i ω j ω x = i 𝑔 j
30 elopab X x y | y = i ω j ω x = i 𝑔 j x y X = x y y = i ω j ω x = i 𝑔 j
31 opeq2 y = x y = x
32 31 adantr y = i ω j ω x = i 𝑔 j x y = x
33 32 eqeq2d y = i ω j ω x = i 𝑔 j X = x y X = x
34 33 biimpd y = i ω j ω x = i 𝑔 j X = x y X = x
35 34 impcom X = x y y = i ω j ω x = i 𝑔 j X = x
36 eqidd y = =
37 36 anim1i y = i ω j ω x = i 𝑔 j = i ω j ω x = i 𝑔 j
38 37 adantl X = x y y = i ω j ω x = i 𝑔 j = i ω j ω x = i 𝑔 j
39 satf00 Sat = y z | z = i ω j ω y = i 𝑔 j
40 26 39 eqtri S = y z | z = i ω j ω y = i 𝑔 j
41 40 eleq2i x S x y z | z = i ω j ω y = i 𝑔 j
42 vex x V
43 0ex V
44 eqeq1 z = z = =
45 eqeq1 y = x y = i 𝑔 j x = i 𝑔 j
46 45 2rexbidv y = x i ω j ω y = i 𝑔 j i ω j ω x = i 𝑔 j
47 44 46 bi2anan9r y = x z = z = i ω j ω y = i 𝑔 j = i ω j ω x = i 𝑔 j
48 42 43 47 opelopaba x y z | z = i ω j ω y = i 𝑔 j = i ω j ω x = i 𝑔 j
49 41 48 bitri x S = i ω j ω x = i 𝑔 j
50 38 49 sylibr X = x y y = i ω j ω x = i 𝑔 j x S
51 35 50 jca X = x y y = i ω j ω x = i 𝑔 j X = x x S
52 51 exlimiv y X = x y y = i ω j ω x = i 𝑔 j X = x x S
53 31 eqeq2d y = X = x y X = x
54 eqeq1 y = y = =
55 54 anbi1d y = y = i ω j ω x = i 𝑔 j = i ω j ω x = i 𝑔 j
56 53 55 anbi12d y = X = x y y = i ω j ω x = i 𝑔 j X = x = i ω j ω x = i 𝑔 j
57 43 56 spcev X = x = i ω j ω x = i 𝑔 j y X = x y y = i ω j ω x = i 𝑔 j
58 49 57 sylan2b X = x x S y X = x y y = i ω j ω x = i 𝑔 j
59 52 58 impbii y X = x y y = i ω j ω x = i 𝑔 j X = x x S
60 59 exbii x y X = x y y = i ω j ω x = i 𝑔 j x X = x x S
61 29 30 60 3bitri X S x X = x x S
62 1 satf0suc z ω S suc z = S z a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
63 62 eleq2d z ω X S suc z X S z a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
64 elun X S z a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u X S z X a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
65 64 a1i z ω X S z a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u X S z X a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
66 elopab X a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u a b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
67 66 a1i z ω X a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u a b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
68 67 orbi2d z ω X S z X a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u X S z a b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
69 63 65 68 3bitrd z ω X S suc z X S z a b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
70 69 adantr z ω X S z x X = x x S z X S suc z X S z a b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
71 simpr z ω X S z x X = x x S z X S z x X = x x S z
72 opeq2 b = a b = a
73 72 eqeq2d b = X = a b X = a
74 73 biimpd b = X = a b X = a
75 74 adantr b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u X = a b X = a
76 75 impcom X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u X = a
77 eqidd X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u =
78 simpr b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
79 78 adantl X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
80 77 79 jca X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
81 76 80 jca X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u X = a = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
82 81 exlimiv b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u X = a = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
83 eqeq1 b = b = =
84 83 anbi1d b = b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
85 73 84 anbi12d b = X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u X = a = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
86 43 85 spcev X = a = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
87 82 86 impbii b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u X = a = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
88 87 exbii a b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u a X = a = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
89 88 a1i z ω a b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u a X = a = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
90 opeq1 x = a x = a
91 90 eqeq2d x = a X = x X = a
92 eqeq1 x = a x = 1 st u 𝑔 1 st v a = 1 st u 𝑔 1 st v
93 92 rexbidv x = a v S z x = 1 st u 𝑔 1 st v v S z a = 1 st u 𝑔 1 st v
94 eqeq1 x = a x = 𝑔 i 1 st u a = 𝑔 i 1 st u
95 94 rexbidv x = a i ω x = 𝑔 i 1 st u i ω a = 𝑔 i 1 st u
96 93 95 orbi12d x = a v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
97 96 rexbidv x = a u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
98 97 anbi2d x = a = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
99 91 98 anbi12d x = a X = x = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u X = a = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
100 99 cbvexvw x X = x = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u a X = a = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
101 89 100 bitr4di z ω a b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u x X = x = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
102 101 adantr z ω X S z x X = x x S z a b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u x X = x = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
103 71 102 orbi12d z ω X S z x X = x x S z X S z a b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u x X = x x S z x X = x = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
104 19.43 x X = x x S z X = x = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x X = x x S z x X = x = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
105 andi X = x x S z = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u X = x x S z X = x = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
106 105 bicomi X = x x S z X = x = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u X = x x S z = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
107 106 exbii x X = x x S z X = x = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x X = x x S z = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
108 104 107 bitr3i x X = x x S z x X = x = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x X = x x S z = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
109 103 108 bitrdi z ω X S z x X = x x S z X S z a b X = a b b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u x X = x x S z = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
110 62 eleq2d z ω x S suc z x S z a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
111 elun x S z a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u x S z x a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u
112 eqeq1 a = x a = 1 st u 𝑔 1 st v x = 1 st u 𝑔 1 st v
113 112 rexbidv a = x v S z a = 1 st u 𝑔 1 st v v S z x = 1 st u 𝑔 1 st v
114 eqeq1 a = x a = 𝑔 i 1 st u x = 𝑔 i 1 st u
115 114 rexbidv a = x i ω a = 𝑔 i 1 st u i ω x = 𝑔 i 1 st u
116 113 115 orbi12d a = x v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
117 116 rexbidv a = x u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
118 83 117 bi2anan9r a = x b = b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
119 42 43 118 opelopaba x a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
120 119 orbi2i x S z x a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u x S z = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
121 111 120 bitri x S z a b | b = u S z v S z a = 1 st u 𝑔 1 st v i ω a = 𝑔 i 1 st u x S z = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
122 110 121 bitrdi z ω x S suc z x S z = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
123 122 anbi2d z ω X = x x S suc z X = x x S z = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
124 123 exbidv z ω x X = x x S suc z x X = x x S z = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
125 124 bicomd z ω x X = x x S z = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x X = x x S suc z
126 125 adantr z ω X S z x X = x x S z x X = x x S z = u S z v S z x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u x X = x x S suc z
127 70 109 126 3bitrd z ω X S z x X = x x S z X S suc z x X = x x S suc z
128 127 ex z ω X S z x X = x x S z X S suc z x X = x x S suc z
129 7 13 19 25 61 128 finds N ω X S N x X = x x S N