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	⊢ ( 𝑈 ∈ ( Fmla ‘ ω ) → ∅ ⊧ 𝑈 )

Proof

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