This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-prv

Description: Define the "proves" relation on a set. A wff is true in a model M if for every valuation s e. ( M ^m _om ) , the interpretation of the wff using the membership relation on M is true. Since |= is defined in terms of the interpretations making the given formula true, it is not defined on the empty "model" M = (/) , since there are no interpretations. In particular, the empty set on the LHS of |= should not be interpreted as the empty model. Statement prv0 shows that our definition yields (/) |= U for all formulas, though of course the formula E. x x = x is not satisfied on the empty model. (Contributed by Mario Carneiro, 14-Jul-2013)

		Ref	Expression
	Assertion	df-prv	$⊢ ⊧ = \{⟨m, u⟩ \| m {Sat}_{\in} u = m^{ω}\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprv	$class ⊧$
1		vm	$setvar m$
2		vu	$setvar u$
3	1	cv	$setvar m$
4		csate	$class {Sat}_{\in}$
5	2	cv	$setvar u$
6	3 5 4	co	$class (m {Sat}_{\in} u)$
7		cmap	$class ↑_{𝑚}$
8		com	$class ω$
9	3 8 7	co	$class (m^{ω})$
10	6 9	wceq	$wff m {Sat}_{\in} u = m^{ω}$
11	10 1 2	copab	$class \{⟨m, u⟩ \| m {Sat}_{\in} u = m^{ω}\}$
12	0 11	wceq	$wff ⊧ = \{⟨m, u⟩ \| m {Sat}_{\in} u = m^{ω}\}$