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 32868 | . 2 class ∀𝑔𝑁𝑈 |
4 | c2o 8125 | . . 3 class 2o | |
5 | 2, 1 | cop 4522 | . . 3 class 〈𝑁, 𝑈〉 |
6 | 4, 5 | cop 4522 | . 2 class 〈2o, 〈𝑁, 𝑈〉〉 |
7 | 3, 6 | wceq 1542 | 1 wff ∀𝑔𝑁𝑈 = 〈2o, 〈𝑁, 𝑈〉〉 |
Colors of variables: wff setvar class |
This definition is referenced by: goaleq12d 32884 gonanegoal 32885 sat1el2xp 32912 fmlaomn0 32923 goaln0 32926 goalrlem 32929 goalr 32930 fmla0disjsuc 32931 fmlasucdisj 32932 satffunlem1lem1 32935 satffunlem2lem1 32937 |
Copyright terms: Public domain | W3C validator |