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	$⊢ U \in Fmla (ω) \to (S \in (\emptyset {Sat}_{\in} U) \to S = \emptyset)$

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		satef	$⊢ (\emptyset \in V \land U \in Fmla (ω) \land S \in (\emptyset {Sat}_{\in} U)) \to S : ω ⟶ \emptyset$
3	1 2	mp3an1	$⊢ (U \in Fmla (ω) \land S \in (\emptyset {Sat}_{\in} U)) \to S : ω ⟶ \emptyset$
4	3	ex	$⊢ U \in Fmla (ω) \to (S \in (\emptyset {Sat}_{\in} U) \to S : ω ⟶ \emptyset)$
5		f00	$⊢ S : ω ⟶ \emptyset \leftrightarrow (S = \emptyset \land ω = \emptyset)$
6	5	simplbi	$⊢ S : ω ⟶ \emptyset \to S = \emptyset$
7	4 6	syl6	$⊢ U \in Fmla (ω) \to (S \in (\emptyset {Sat}_{\in} U) \to S = \emptyset)$

Metamath Proof Explorer