Theorem sate0fv0

Description: A simplified satisfaction predicate as function over wff codes over an empty model is an empty set. (Contributed by AV, 31-Oct-2023)

	Ref	Expression
Assertion	sate0fv0	⊢ ( 𝑈 ∈ ( Fmla ‘ ω ) → ( 𝑆 ∈ ( ∅ Sat∈ 𝑈 ) → 𝑆 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		satef	⊢ ( ( ∅ ∈ V ∧ 𝑈 ∈ ( Fmla ‘ ω ) ∧ 𝑆 ∈ ( ∅ Sat∈ 𝑈 ) ) → 𝑆 : ω ⟶ ∅ )
3	1 2	mp3an1	⊢ ( ( 𝑈 ∈ ( Fmla ‘ ω ) ∧ 𝑆 ∈ ( ∅ Sat∈ 𝑈 ) ) → 𝑆 : ω ⟶ ∅ )
4	3	ex	⊢ ( 𝑈 ∈ ( Fmla ‘ ω ) → ( 𝑆 ∈ ( ∅ Sat∈ 𝑈 ) → 𝑆 : ω ⟶ ∅ ) )
5		f00	⊢ ( 𝑆 : ω ⟶ ∅ ↔ ( 𝑆 = ∅ ∧ ω = ∅ ) )
6	5	simplbi	⊢ ( 𝑆 : ω ⟶ ∅ → 𝑆 = ∅ )
7	4 6	syl6	⊢ ( 𝑈 ∈ ( Fmla ‘ ω ) → ( 𝑆 ∈ ( ∅ Sat∈ 𝑈 ) → 𝑆 = ∅ ) )