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	⊢ ⊧ = { ⟨ 𝑚 , 𝑢 ⟩ ∣ ( 𝑚 Sat∈ 𝑢 ) = ( 𝑚 ↑m ω ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprv	⊢ ⊧
1		vm	⊢ 𝑚
2		vu	⊢ 𝑢
3	1	cv	⊢ 𝑚
4		csate	⊢ Sat∈
5	2	cv	⊢ 𝑢
6	3 5 4	co	⊢ ( 𝑚 Sat∈ 𝑢 )
7		cmap	⊢ ↑m
8		com	⊢ ω
9	3 8 7	co	⊢ ( 𝑚 ↑m ω )
10	6 9	wceq	⊢ ( 𝑚 Sat∈ 𝑢 ) = ( 𝑚 ↑m ω )
11	10 1 2	copab	⊢ { ⟨ 𝑚 , 𝑢 ⟩ ∣ ( 𝑚 Sat∈ 𝑢 ) = ( 𝑚 ↑m ω ) }
12	0 11	wceq	⊢ ⊧ = { ⟨ 𝑚 , 𝑢 ⟩ ∣ ( 𝑚 Sat∈ 𝑢 ) = ( 𝑚 ↑m ω ) }