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∪xy|y=∅∧∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡uxy|y=∅∧∃i∈ω∃j∈ωx=i∈𝑔j↾suc⁡ω

Proof

Step Hyp Ref Expression
1 0ex ⊢∅∈V
2 satf ⊢∅∈V∧∅∈V→∅Sat∅=rec⁡f∈V⟼f∪xy|∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡uxy|∃i∈ω∃j∈ωx=i∈𝑔j∧y=a∈∅ω|a⁡i∅a⁡j↾suc⁡ω
3 1 1 2 mp2an ⊢∅Sat∅=rec⁡f∈V⟼f∪xy|∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡uxy|∃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 ⊢∅ω∖2nd⁡u∩2nd⁡v=∅∖2nd⁡u∩2nd⁡v
9 0dif ⊢∅∖2nd⁡u∩2nd⁡v=∅
10 8 9 eqtri ⊢∅ω∖2nd⁡u∩2nd⁡v=∅
11 10 eqeq2i ⊢y=∅ω∖2nd⁡u∩2nd⁡v↔y=∅
12 11 anbi2i ⊢x=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v↔x=1st⁡u⊼𝑔1st⁡v∧y=∅
13 12 rexbii ⊢∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v↔∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅
14 r19.41v ⊢∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅↔∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅
15 13 14 bitri ⊢∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v↔∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅
16 7 rabeqi ⊢a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u=a∈∅|∀z∈∅iz∪a↾ω∖i∈2nd⁡u
17 rab0 ⊢a∈∅|∀z∈∅iz∪a↾ω∖i∈2nd⁡u=∅
18 16 17 eqtri ⊢a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u=∅
19 18 eqeq2i ⊢y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u↔y=∅
20 19 anbi2i ⊢x=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u↔x=∀𝑔i1st⁡u∧y=∅
21 20 rexbii ⊢∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u↔∃i∈ωx=∀𝑔i1st⁡u∧y=∅
22 r19.41v ⊢∃i∈ωx=∀𝑔i1st⁡u∧y=∅↔∃i∈ωx=∀𝑔i1st⁡u∧y=∅
23 21 22 bitri ⊢∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u↔∃i∈ωx=∀𝑔i1st⁡u∧y=∅
24 15 23 orbi12i ⊢∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u↔∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅∨∃i∈ωx=∀𝑔i1st⁡u∧y=∅
25 24 rexbii ⊢∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u↔∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅∨∃i∈ωx=∀𝑔i1st⁡u∧y=∅
26 andir ⊢∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=∅↔∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅∨∃i∈ωx=∀𝑔i1st⁡u∧y=∅
27 26 bicomi ⊢∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅∨∃i∈ωx=∀𝑔i1st⁡u∧y=∅↔∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=∅
28 27 rexbii ⊢∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅∨∃i∈ωx=∀𝑔i1st⁡u∧y=∅↔∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=∅
29 r19.41v ⊢∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=∅↔∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=∅
30 25 28 29 3bitri ⊢∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u↔∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=∅
31 30 biancomi ⊢∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u↔y=∅∧∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡u
32 31 opabbii ⊢xy|∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u=xy|y=∅∧∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡u
33 32 uneq2i ⊢f∪xy|∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u=f∪xy|y=∅∧∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡u
34 33 mpteq2i ⊢f∈V⟼f∪xy|∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u=f∈V⟼f∪xy|y=∅∧∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡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 ⊢xy|∃i∈ω∃j∈ωx=i∈𝑔j∧y=a∈∅ω|a⁡i∅a⁡j=xy|y=∅∧∃i∈ω∃j∈ωx=i∈𝑔j
45 rdgeq12 ⊢f∈V⟼f∪xy|∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡u=f∈V⟼f∪xy|y=∅∧∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧xy|∃i∈ω∃j∈ωx=i∈𝑔j∧y=a∈∅ω|a⁡i∅a⁡j=xy|y=∅∧∃i∈ω∃j∈ωx=i∈𝑔j→rec⁡f∈V⟼f∪xy|∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡uxy|∃i∈ω∃j∈ωx=i∈𝑔j∧y=a∈∅ω|a⁡i∅a⁡j=rec⁡f∈V⟼f∪xy|y=∅∧∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡uxy|y=∅∧∃i∈ω∃j∈ωx=i∈𝑔j
46 34 44 45 mp2an ⊢rec⁡f∈V⟼f∪xy|∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡uxy|∃i∈ω∃j∈ωx=i∈𝑔j∧y=a∈∅ω|a⁡i∅a⁡j=rec⁡f∈V⟼f∪xy|y=∅∧∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡uxy|y=∅∧∃i∈ω∃j∈ωx=i∈𝑔j
47 46 reseq1i ⊢rec⁡f∈V⟼f∪xy|∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∧y=∅ω∖2nd⁡u∩2nd⁡v∨∃i∈ωx=∀𝑔i1st⁡u∧y=a∈∅ω|∀z∈∅iz∪a↾ω∖i∈2nd⁡uxy|∃i∈ω∃j∈ωx=i∈𝑔j∧y=a∈∅ω|a⁡i∅a⁡j↾suc⁡ω=rec⁡f∈V⟼f∪xy|y=∅∧∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡uxy|y=∅∧∃i∈ω∃j∈ωx=i∈𝑔j↾suc⁡ω
48 3 47 eqtri ⊢∅Sat∅=rec⁡f∈V⟼f∪xy|y=∅∧∃u∈f∃v∈fx=1st⁡u⊼𝑔1st⁡v∨∃i∈ωx=∀𝑔i1st⁡uxy|y=∅∧∃i∈ω∃j∈ωx=i∈𝑔j↾suc⁡ω