Metamath Proof Explorer


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
|- |g = ( x e. ( _V X. _V ) |-> <. 1o , x >. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgna
 |-  |g
1 vx
 |-  x
2 cvv
 |-  _V
3 2 2 cxp
 |-  ( _V X. _V )
4 c1o
 |-  1o
5 1 cv
 |-  x
6 4 5 cop
 |-  <. 1o , x >.
7 1 3 6 cmpt
 |-  ( x e. ( _V X. _V ) |-> <. 1o , x >. )
8 0 7 wceq
 |-  |g = ( x e. ( _V X. _V ) |-> <. 1o , x >. )