Metamath Proof Explorer

Theorem sate0

Description: The simplified satisfaction predicate for any wff code over an empty model. (Contributed by AV, 6-Oct-2023) (Revised by AV, 5-Nov-2023)

		Ref	Expression
	Assertion	sate0	$⊢ U \in V \to \emptyset {Sat}_{\in} U = (\emptyset Sat \emptyset) (ω) (U)$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		satefv	$⊢ (\emptyset \in V \land U \in V) \to \emptyset {Sat}_{\in} U = (\emptyset Sat (E \cap (\emptyset \times \emptyset))) (ω) (U)$
3	1 2	mpan	$⊢ U \in V \to \emptyset {Sat}_{\in} U = (\emptyset Sat (E \cap (\emptyset \times \emptyset))) (ω) (U)$
4		xp0	$⊢ \emptyset \times \emptyset = \emptyset$
5	4	ineq2i	$⊢ E \cap (\emptyset \times \emptyset) = E \cap \emptyset$
6		in0	$⊢ E \cap \emptyset = \emptyset$
7	5 6	eqtri	$⊢ E \cap (\emptyset \times \emptyset) = \emptyset$
8	7	oveq2i	$⊢ \emptyset Sat (E \cap (\emptyset \times \emptyset)) = \emptyset Sat \emptyset$
9	8	fveq1i	$⊢ (\emptyset Sat (E \cap (\emptyset \times \emptyset))) (ω) = (\emptyset Sat \emptyset) (ω)$
10	9	fveq1i	$⊢ (\emptyset Sat (E \cap (\emptyset \times \emptyset))) (ω) (U) = (\emptyset Sat \emptyset) (ω) (U)$
11	3 10	eqtrdi	$⊢ U \in V \to \emptyset {Sat}_{\in} U = (\emptyset Sat \emptyset) (ω) (U)$