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 SatE u ) = ( m ^m _om ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprv	|- |=
1		vm	|- m
2		vu	|- u
3	1	cv	|- m
4		csate	|- SatE
5	2	cv	|- u
6	3 5 4	co	|- ( m SatE u )
7		cmap	|- ^m
8		com	|- _om
9	3 8 7	co	|- ( m ^m _om )
10	6 9	wceq	|- ( m SatE u ) = ( m ^m _om )
11	10 1 2	copab	|- { <. m , u >. | ( m SatE u ) = ( m ^m _om ) }
12	0 11	wceq	|- |= = { <. m , u >. | ( m SatE u ) = ( m ^m _om ) }