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 >. ) |
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 >. ) |