Definition df-prv 30596

Description: Define the "proves" relation on a set. A wff is true in a model 𝑀 if for every valuation 𝑠 ∈ (𝑀 ↑_𝑚 ω), the interpretation of the wff using the membership relation on 𝑀 is true. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

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

Distinct variable group:   𝑢,𝑚

Detailed syntax breakdown of Definition df-prv

Step	Hyp	Ref	Expression
1		cprv 30575	. 2 class ⊧
2		vm	. . . . . 6 setvar 𝑚
3	2	cv 1474	. . . . 5 class 𝑚
4		vu	. . . . . 6 setvar 𝑢
5	4	cv 1474	. . . . 5 class 𝑢
6		csate 30574	. . . . 5 class Sat∈
7	3, 5, 6	co 6549	. . . 4 class (𝑚 Sat∈ 𝑢)
8		com 6957	. . . . 5 class ω
9		cmap 7744	. . . . 5 class ↑𝑚
10	3, 8, 9	co 6549	. . . 4 class (𝑚 ↑𝑚 ω)
11	7, 10	wceq 1475	. . 3 wff (𝑚 Sat∈ 𝑢) = (𝑚 ↑𝑚 ω)
12	11, 2, 4	copab 4642	. 2 class {⟨𝑚, 𝑢⟩ ∣ (𝑚 Sat∈ 𝑢) = (𝑚 ↑𝑚 ω)}
13	1, 12	wceq 1475	1 wff ⊧ = {⟨𝑚, 𝑢⟩ ∣ (𝑚 Sat∈ 𝑢) = (𝑚 ↑𝑚 ω)}

This definition is referenced by: (None)