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 | |- e.g = ( x e. ( _om X. _om ) |-> <. (/) , x >. ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cgoe | |- e.g |
|
| 1 | vx | |- x |
|
| 2 | com | |- _om |
|
| 3 | 2 2 | cxp | |- ( _om X. _om ) |
| 4 | c0 | |- (/) |
|
| 5 | 1 | cv | |- x |
| 6 | 4 5 | cop | |- <. (/) , x >. |
| 7 | 1 3 6 | cmpt | |- ( x e. ( _om X. _om ) |-> <. (/) , x >. ) |
| 8 | 0 7 | wceq | |- e.g = ( x e. ( _om X. _om ) |-> <. (/) , x >. ) |