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 33203 | . 2 class ∀𝑔𝑁𝑈 |
4 | c2o 8262 | . . 3 class 2o | |
5 | 2, 1 | cop 4565 | . . 3 class 〈𝑁, 𝑈〉 |
6 | 4, 5 | cop 4565 | . 2 class 〈2o, 〈𝑁, 𝑈〉〉 |
7 | 3, 6 | wceq 1539 | 1 wff ∀𝑔𝑁𝑈 = 〈2o, 〈𝑁, 𝑈〉〉 |
Colors of variables: wff setvar class |
This definition is referenced by: goaleq12d 33219 gonanegoal 33220 sat1el2xp 33247 fmlaomn0 33258 goaln0 33261 goalrlem 33264 goalr 33265 fmla0disjsuc 33266 fmlasucdisj 33267 satffunlem1lem1 33270 satffunlem2lem1 33272 |
Copyright terms: Public domain | W3C validator |