Definition df-prv 35351

Description: Define the "proves" relation on a set. A wff is true in a model 𝑀 if for every valuation 𝑠 ∈ (𝑀 ↑_m ω), the interpretation of the wff using the membership relation on 𝑀 is true. Since ⊧ is defined in terms of the interpretations making the given formula true, it is not defined on the empty "model" 𝑀 = ∅, since there are no interpretations. In particular, the empty set on the LHS of ⊧ should not be interpreted as the empty model. Statement prv0 35435 shows that our definition yields ∅⊧𝑈 for all formulas, though of course the formula ∃𝑥𝑥 = 𝑥 is not satisfied on the empty model. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-prv	⊢ ⊧ = {⟨𝑚, 𝑢⟩ ∣ (𝑚 Sat∈ 𝑢) = (𝑚 ↑m ω)}

Distinct variable group:   𝑢,𝑚

Detailed syntax breakdown of Definition df-prv

Step	Hyp	Ref	Expression
1		cprv 35344	. 2 class ⊧
2		vm	. . . . . 6 setvar 𝑚
3	2	cv 1539	. . . . 5 class 𝑚
4		vu	. . . . . 6 setvar 𝑢
5	4	cv 1539	. . . . 5 class 𝑢
6		csate 35343	. . . . 5 class Sat∈
7	3, 5, 6	co 7431	. . . 4 class (𝑚 Sat∈ 𝑢)
8		com 7887	. . . . 5 class ω
9		cmap 8866	. . . . 5 class ↑m
10	3, 8, 9	co 7431	. . . 4 class (𝑚 ↑m ω)
11	7, 10	wceq 1540	. . 3 wff (𝑚 Sat∈ 𝑢) = (𝑚 ↑m ω)
12	11, 2, 4	copab 5205	. 2 class {⟨𝑚, 𝑢⟩ ∣ (𝑚 Sat∈ 𝑢) = (𝑚 ↑m ω)}
13	1, 12	wceq 1540	1 wff ⊧ = {⟨𝑚, 𝑢⟩ ∣ (𝑚 Sat∈ 𝑢) = (𝑚 ↑m ω)}

This definition is referenced by:  prv  35433