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 33317 | . 2 class ∀𝑔𝑁𝑈 |
4 | c2o 8303 | . . 3 class 2o | |
5 | 2, 1 | cop 4571 | . . 3 class 〈𝑁, 𝑈〉 |
6 | 4, 5 | cop 4571 | . 2 class 〈2o, 〈𝑁, 𝑈〉〉 |
7 | 3, 6 | wceq 1538 | 1 wff ∀𝑔𝑁𝑈 = 〈2o, 〈𝑁, 𝑈〉〉 |
Colors of variables: wff setvar class |
This definition is referenced by: goaleq12d 33333 gonanegoal 33334 sat1el2xp 33361 fmlaomn0 33372 goaln0 33375 goalrlem 33378 goalr 33379 fmla0disjsuc 33380 fmlasucdisj 33381 satffunlem1lem1 33384 satffunlem2lem1 33386 |
Copyright terms: Public domain | W3C validator |