Metamath Proof Explorer

Theorem prv0

Description: Every wff encoded as U is true in an "empty model" ( M = (/) ). Since |= is defined in terms of the interpretations making the given formula true, it is not defined on the "empty model", since there are no interpretations. In particular, the empty set on the LHS of |= should not be interpreted as the empty model, because E. x x = x is not satisfied on the empty model. (Contributed by AV, 19-Nov-2023)

Ref Expression
Assertion prv0 ⊢ U ∈ Fmla ⁡ ω → ∅ ⊧ U

Proof

Step Hyp Ref Expression
1 sate0 ⊢ U ∈ Fmla ⁡ ω → ∅ Sat ∈ U = ∅ Sat ∅ ⁡ ω ⁡ U
2 peano1 ⊢ ∅ ∈ ω
3 2 n0ii ⊢ ¬ ω = ∅
4 3 intnan ⊢ ¬ x = ∅ ∧ ω = ∅
5 4 a1i ⊢ U ∈ Fmla ⁡ ω → ¬ x = ∅ ∧ ω = ∅
6 f00 ⊢ x : ω ⟶ ∅ ↔ x = ∅ ∧ ω = ∅
7 5 6 sylnibr ⊢ U ∈ Fmla ⁡ ω → ¬ x : ω ⟶ ∅
8 0ex ⊢ ∅ ∈ V
9 8 8 pm3.2i ⊢ ∅ ∈ V ∧ ∅ ∈ V
10 satfvel ⊢ ∅ ∈ V ∧ ∅ ∈ V ∧ U ∈ Fmla ⁡ ω ∧ x ∈ ∅ Sat ∅ ⁡ ω ⁡ U → x : ω ⟶ ∅
11 9 10 mp3an1 ⊢ U ∈ Fmla ⁡ ω ∧ x ∈ ∅ Sat ∅ ⁡ ω ⁡ U → x : ω ⟶ ∅
12 7 11 mtand ⊢ U ∈ Fmla ⁡ ω → ¬ x ∈ ∅ Sat ∅ ⁡ ω ⁡ U
13 12 alrimiv ⊢ U ∈ Fmla ⁡ ω → ∀ x ¬ x ∈ ∅ Sat ∅ ⁡ ω ⁡ U
14 eq0 ⊢ ∅ Sat ∅ ⁡ ω ⁡ U = ∅ ↔ ∀ x ¬ x ∈ ∅ Sat ∅ ⁡ ω ⁡ U
15 13 14 sylibr ⊢ U ∈ Fmla ⁡ ω → ∅ Sat ∅ ⁡ ω ⁡ U = ∅
16 1 15 eqtrd ⊢ U ∈ Fmla ⁡ ω → ∅ Sat ∈ U = ∅
17 prv ⊢ ∅ ∈ V ∧ U ∈ Fmla ⁡ ω → ∅ ⊧ U ↔ ∅ Sat ∈ U = ∅ ω
18 8 17 mpan ⊢ U ∈ Fmla ⁡ ω → ∅ ⊧ U ↔ ∅ Sat ∈ U = ∅ ω
19 2 ne0ii ⊢ ω ≠ ∅
20 map0b ⊢ ω ≠ ∅ → ∅ ω = ∅
21 19 20 mp1i ⊢ U ∈ Fmla ⁡ ω → ∅ ω = ∅
22 21 eqeq2d ⊢ U ∈ Fmla ⁡ ω → ∅ Sat ∈ U = ∅ ω ↔ ∅ Sat ∈ U = ∅
23 18 22 bitrd ⊢ U ∈ Fmla ⁡ ω → ∅ ⊧ U ↔ ∅ Sat ∈ U = ∅
24 16 23 mpbird ⊢ U ∈ Fmla ⁡ ω → ∅ ⊧ U