Definition df-prv 32586

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 32670 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 32579	. 2 class ⊧
2		vm	. . . . . 6 setvar 𝑚
3	2	cv 1530	. . . . 5 class 𝑚
4		vu	. . . . . 6 setvar 𝑢
5	4	cv 1530	. . . . 5 class 𝑢
6		csate 32578	. . . . 5 class Sat∈
7	3, 5, 6	co 7148	. . . 4 class (𝑚 Sat∈ 𝑢)
8		com 7572	. . . . 5 class ω
9		cmap 8398	. . . . 5 class ↑m
10	3, 8, 9	co 7148	. . . 4 class (𝑚 ↑m ω)
11	7, 10	wceq 1531	. . 3 wff (𝑚 Sat∈ 𝑢) = (𝑚 ↑m ω)
12	11, 2, 4	copab 5119	. 2 class {⟨𝑚, 𝑢⟩ ∣ (𝑚 Sat∈ 𝑢) = (𝑚 ↑m ω)}
13	1, 12	wceq 1531	1 wff ⊧ = {⟨𝑚, 𝑢⟩ ∣ (𝑚 Sat∈ 𝑢) = (𝑚 ↑m ω)}

This definition is referenced by:  prv  32668