Description: Define the Godel-set of implication. Here the arguments U and V are also Godel-sets corresponding to smaller formulas. Note that this is aclass expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-goim | |- ->g = ( u e. _V , v e. _V |-> ( u |g -.g v ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cgoi | |- ->g |
|
| 1 | vu | |- u |
|
| 2 | cvv | |- _V |
|
| 3 | vv | |- v |
|
| 4 | 1 | cv | |- u |
| 5 | cgna | |- |g |
|
| 6 | 3 | cv | |- v |
| 7 | 6 | cgon | |- -.g v |
| 8 | 4 7 5 | co | |- ( u |g -.g v ) |
| 9 | 1 3 2 2 8 | cmpo | |- ( u e. _V , v e. _V |-> ( u |g -.g v ) ) |
| 10 | 0 9 | wceq | |- ->g = ( u e. _V , v e. _V |-> ( u |g -.g v ) ) |