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	$$⊢\vDash =\left\{⟨m,u⟩|m{\mathrm{Sat}}_{\in }u=m^{\mathrm{\omega }}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprv	$$class\vDash$$
1		vm	$$setvarm$$
2		vu	$$setvaru$$
3	1	cv	$$setvarm$$
4		csate	$$class{\mathrm{Sat}}_{\in }$$
5	2	cv	$$setvaru$$
6	3 5 4	co	$$class\left(m{\mathrm{Sat}}_{\in }u\right)$$
7		cmap	$$class{\uparrow }_{𝑚}$$
8		com	$$class\mathrm{\omega }$$
9	3 8 7	co	$$class\left(m^{\mathrm{\omega }}\right)$$
10	6 9	wceq	$$wffm{\mathrm{Sat}}_{\in }u=m^{\mathrm{\omega }}$$
11	10 1 2	copab	$$class\left\{⟨m,u⟩|m{\mathrm{Sat}}_{\in }u=m^{\mathrm{\omega }}\right\}$$
12	0 11	wceq	$$wff\vDash =\left\{⟨m,u⟩|m{\mathrm{Sat}}_{\in }u=m^{\mathrm{\omega }}\right\}$$