Definition df-gona

Description: Define the Godel-set for the Sheffer stroke NAND. Here the arguments x = <. U , V >. are also Godel-sets corresponding to smaller formulas. (Contributed by Mario Carneiro, 14-Jul-2013)

	Ref	Expression
Assertion	df-gona	⊢ ⊼𝑔 = ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgna	⊢ ⊼𝑔
1		vx	⊢ 𝑥
2		cvv	⊢ V
3	2 2	cxp	⊢ ( V × V )
4		c1o	⊢ 1o
5	1	cv	⊢ 𝑥
6	4 5	cop	⊢ ⟨ 1o , 𝑥 ⟩
7	1 3 6	cmpt	⊢ ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ )
8	0 7	wceq	⊢ ⊼𝑔 = ( 𝑥 ∈ ( V × V ) ↦ ⟨ 1o , 𝑥 ⟩ )