| Mathbox for Mario Carneiro |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-goal | Structured version Visualization version GIF version | ||
| Description: Define the Godel-set of universal quantification. Here 𝑁 ∈ ω corresponds to vN , and 𝑈 represents another formula, and this expression is [∀𝑥𝜑] = ∀𝑔𝑁𝑈 where 𝑥 is the 𝑁-th variable, 𝑈 = [𝜑] is the code for 𝜑. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.) |
| Ref | Expression |
|---|---|
| df-goal | ⊢ ∀𝑔𝑁𝑈 = 〈2o, 〈𝑁, 𝑈〉〉 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cU | . . 3 class 𝑈 | |
| 2 | cN | . . 3 class 𝑁 | |
| 3 | 1, 2 | cgol 35340 | . 2 class ∀𝑔𝑁𝑈 |
| 4 | c2o 8500 | . . 3 class 2o | |
| 5 | 2, 1 | cop 4632 | . . 3 class 〈𝑁, 𝑈〉 |
| 6 | 4, 5 | cop 4632 | . 2 class 〈2o, 〈𝑁, 𝑈〉〉 |
| 7 | 3, 6 | wceq 1540 | 1 wff ∀𝑔𝑁𝑈 = 〈2o, 〈𝑁, 𝑈〉〉 |
| Colors of variables: wff setvar class |
| This definition is referenced by: goaleq12d 35356 gonanegoal 35357 sat1el2xp 35384 fmlaomn0 35395 goaln0 35398 goalrlem 35401 goalr 35402 fmla0disjsuc 35403 fmlasucdisj 35404 satffunlem1lem1 35407 satffunlem2lem1 35409 |
| Copyright terms: Public domain | W3C validator |