Description: Define the Godel-set of conjunction. Here the arguments U and V are also Godel-sets corresponding to smaller formulas. (Contributed by Mario Carneiro, 14-Jul-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-goan | |- /\g = ( u e. _V , v e. _V |-> -.g ( u |g v ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cgoa | |- /\g |
|
| 1 | vu | |- u |
|
| 2 | cvv | |- _V |
|
| 3 | vv | |- v |
|
| 4 | 1 | cv | |- u |
| 5 | cgna | |- |g |
|
| 6 | 3 | cv | |- v |
| 7 | 4 6 5 | co | |- ( u |g v ) |
| 8 | 7 | cgon | |- -.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 ) ) |