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 ⁡ ω