Definition df-goel

Description: Define the Godel-set of membership. Here the arguments x = <. N , P >. correspond to v_N and v_P , so ( (/) e.g 1o ) actually means v_0 e. v_1 , not 0 e. 1 . (Contributed by Mario Carneiro, 14-Jul-2013)

	Ref	Expression
Assertion	df-goel	$$⊢{\in }_{𝑔}=\left(x\in \left(\mathrm{\omega }\times \mathrm{\omega }\right)⟼⟨\varnothing ,x⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgoe	$$class{\in }_{𝑔}$$
1		vx	$$setvarx$$
2		com	$$class\mathrm{\omega }$$
3	2 2	cxp	$$class\left(\mathrm{\omega }\times \mathrm{\omega }\right)$$
4		c0	$$class\varnothing$$
5	1	cv	$$setvarx$$
6	4 5	cop	$$class⟨\varnothing ,x⟩$$
7	1 3 6	cmpt	$$class\left(x\in \left(\mathrm{\omega }\times \mathrm{\omega }\right)⟼⟨\varnothing ,x⟩\right)$$
8	0 7	wceq	$$wff{\in }_{𝑔}=\left(x\in \left(\mathrm{\omega }\times \mathrm{\omega }\right)⟼⟨\varnothing ,x⟩\right)$$