Metamath Proof Explorer

Theorem satf0n0

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

Ref Expression
Assertion satf0n0 ⊢ N ∈ ω → ∅ ∉ ∅ Sat ∅ ⁡ N

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ x = ∅ → ∅ Sat ∅ ⁡ x = ∅ Sat ∅ ⁡ ∅
2 1 eleq2d ⊢ x = ∅ → ∅ ∈ ∅ Sat ∅ ⁡ x ↔ ∅ ∈ ∅ Sat ∅ ⁡ ∅
3 2 notbid ⊢ x = ∅ → ¬ ∅ ∈ ∅ Sat ∅ ⁡ x ↔ ¬ ∅ ∈ ∅ Sat ∅ ⁡ ∅
4 fveq2 ⊢ x = y → ∅ Sat ∅ ⁡ x = ∅ Sat ∅ ⁡ y
5 4 eleq2d ⊢ x = y → ∅ ∈ ∅ Sat ∅ ⁡ x ↔ ∅ ∈ ∅ Sat ∅ ⁡ y
6 5 notbid ⊢ x = y → ¬ ∅ ∈ ∅ Sat ∅ ⁡ x ↔ ¬ ∅ ∈ ∅ Sat ∅ ⁡ y
7 fveq2 ⊢ x = suc ⁡ y → ∅ Sat ∅ ⁡ x = ∅ Sat ∅ ⁡ suc ⁡ y
8 7 eleq2d ⊢ x = suc ⁡ y → ∅ ∈ ∅ Sat ∅ ⁡ x ↔ ∅ ∈ ∅ Sat ∅ ⁡ suc ⁡ y
9 8 notbid ⊢ x = suc ⁡ y → ¬ ∅ ∈ ∅ Sat ∅ ⁡ x ↔ ¬ ∅ ∈ ∅ Sat ∅ ⁡ suc ⁡ y
10 fveq2 ⊢ x = N → ∅ Sat ∅ ⁡ x = ∅ Sat ∅ ⁡ N
11 10 eleq2d ⊢ x = N → ∅ ∈ ∅ Sat ∅ ⁡ x ↔ ∅ ∈ ∅ Sat ∅ ⁡ N
12 11 notbid ⊢ x = N → ¬ ∅ ∈ ∅ Sat ∅ ⁡ x ↔ ¬ ∅ ∈ ∅ Sat ∅ ⁡ N
13 0nelopab ⊢ ¬ ∅ ∈ x y | y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j
14 satf00 ⊢ ∅ Sat ∅ ⁡ ∅ = x y | y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j
15 14 eleq2i ⊢ ∅ ∈ ∅ Sat ∅ ⁡ ∅ ↔ ∅ ∈ x y | y = ∅ ∧ ∃ i ∈ ω ∃ j ∈ ω x = i ∈ 𝑔 j
16 13 15 mtbir ⊢ ¬ ∅ ∈ ∅ Sat ∅ ⁡ ∅
17 simpr ⊢ y ∈ ω ∧ ¬ ∅ ∈ ∅ Sat ∅ ⁡ y → ¬ ∅ ∈ ∅ Sat ∅ ⁡ y
18 0nelopab ⊢ ¬ ∅ ∈ x z | z = ∅ ∧ ∃ u ∈ ∅ Sat ∅ ⁡ y ∃ v ∈ ∅ Sat ∅ ⁡ y x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u
19 ioran ⊢ ¬ ∅ ∈ ∅ Sat ∅ ⁡ y ∨ ∅ ∈ x z | z = ∅ ∧ ∃ u ∈ ∅ Sat ∅ ⁡ y ∃ v ∈ ∅ Sat ∅ ⁡ y x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ↔ ¬ ∅ ∈ ∅ Sat ∅ ⁡ y ∧ ¬ ∅ ∈ x z | z = ∅ ∧ ∃ u ∈ ∅ Sat ∅ ⁡ y ∃ v ∈ ∅ Sat ∅ ⁡ y x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u
20 17 18 19 sylanblrc ⊢ y ∈ ω ∧ ¬ ∅ ∈ ∅ Sat ∅ ⁡ y → ¬ ∅ ∈ ∅ Sat ∅ ⁡ y ∨ ∅ ∈ x z | z = ∅ ∧ ∃ u ∈ ∅ Sat ∅ ⁡ y ∃ v ∈ ∅ Sat ∅ ⁡ y x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u
21 eqid ⊢ ∅ Sat ∅ = ∅ Sat ∅
22 21 satf0suc ⊢ y ∈ ω → ∅ Sat ∅ ⁡ suc ⁡ y = ∅ Sat ∅ ⁡ y ∪ x z | z = ∅ ∧ ∃ u ∈ ∅ Sat ∅ ⁡ y ∃ v ∈ ∅ Sat ∅ ⁡ y x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u
23 22 adantr ⊢ y ∈ ω ∧ ¬ ∅ ∈ ∅ Sat ∅ ⁡ y → ∅ Sat ∅ ⁡ suc ⁡ y = ∅ Sat ∅ ⁡ y ∪ x z | z = ∅ ∧ ∃ u ∈ ∅ Sat ∅ ⁡ y ∃ v ∈ ∅ Sat ∅ ⁡ y x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u
24 23 eleq2d ⊢ y ∈ ω ∧ ¬ ∅ ∈ ∅ Sat ∅ ⁡ y → ∅ ∈ ∅ Sat ∅ ⁡ suc ⁡ y ↔ ∅ ∈ ∅ Sat ∅ ⁡ y ∪ x z | z = ∅ ∧ ∃ u ∈ ∅ Sat ∅ ⁡ y ∃ v ∈ ∅ Sat ∅ ⁡ y x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u
25 elun ⊢ ∅ ∈ ∅ Sat ∅ ⁡ y ∪ x z | z = ∅ ∧ ∃ u ∈ ∅ Sat ∅ ⁡ y ∃ v ∈ ∅ Sat ∅ ⁡ y x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u ↔ ∅ ∈ ∅ Sat ∅ ⁡ y ∨ ∅ ∈ x z | z = ∅ ∧ ∃ u ∈ ∅ Sat ∅ ⁡ y ∃ v ∈ ∅ Sat ∅ ⁡ y x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u
26 24 25 bitrdi ⊢ y ∈ ω ∧ ¬ ∅ ∈ ∅ Sat ∅ ⁡ y → ∅ ∈ ∅ Sat ∅ ⁡ suc ⁡ y ↔ ∅ ∈ ∅ Sat ∅ ⁡ y ∨ ∅ ∈ x z | z = ∅ ∧ ∃ u ∈ ∅ Sat ∅ ⁡ y ∃ v ∈ ∅ Sat ∅ ⁡ y x = 1 st ⁡ u ⊼ 𝑔 1 st ⁡ v ∨ ∃ i ∈ ω x = ∀ 𝑔 i 1 st ⁡ u
27 20 26 mtbird ⊢ y ∈ ω ∧ ¬ ∅ ∈ ∅ Sat ∅ ⁡ y → ¬ ∅ ∈ ∅ Sat ∅ ⁡ suc ⁡ y
28 27 ex ⊢ y ∈ ω → ¬ ∅ ∈ ∅ Sat ∅ ⁡ y → ¬ ∅ ∈ ∅ Sat ∅ ⁡ suc ⁡ y
29 3 6 9 12 16 28 finds ⊢ N ∈ ω → ¬ ∅ ∈ ∅ Sat ∅ ⁡ N
30 df-nel ⊢ ∅ ∉ ∅ Sat ∅ ⁡ N ↔ ¬ ∅ ∈ ∅ Sat ∅ ⁡ N
31 29 30 sylibr ⊢ N ∈ ω → ∅ ∉ ∅ Sat ∅ ⁡ N