This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ∈_𝑔 = ( 𝑥 ∈ ( ω × ω ) ↦ ⟨ ∅ , 𝑥 ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgoe	⊢ ∈_𝑔
1		vx	⊢ 𝑥
2		com	⊢ ω
3	2 2	cxp	⊢ ( ω × ω )
4		c0	⊢ ∅
5	1	cv	⊢ 𝑥
6	4 5	cop	⊢ ⟨ ∅ , 𝑥 ⟩
7	1 3 6	cmpt	⊢ ( 𝑥 ∈ ( ω × ω ) ↦ ⟨ ∅ , 𝑥 ⟩ )
8	0 7	wceq	⊢ ∈_𝑔 = ( 𝑥 ∈ ( ω × ω ) ↦ ⟨ ∅ , 𝑥 ⟩ )