Description: Define the Godel-set of disjunction. 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-goor | |- \/g = ( u e. _V , v e. _V |-> ( -.g u ->g v ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cgoo | |- \/g |
|
| 1 | vu | |- u |
|
| 2 | cvv | |- _V |
|
| 3 | vv | |- v |
|
| 4 | 1 | cv | |- u |
| 5 | 4 | cgon | |- -.g u |
| 6 | cgoi | |- ->g |
|
| 7 | 3 | cv | |- v |
| 8 | 5 7 6 | co | |- ( -.g u ->g v ) |
| 9 | 1 3 2 2 8 | cmpo | |- ( u e. _V , v e. _V |-> ( -.g u ->g v ) ) |
| 10 | 0 9 | wceq | |- \/g = ( u e. _V , v e. _V |-> ( -.g u ->g v ) ) |