![]() |
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 34321 | . 2 class ∀𝑔𝑁𝑈 |
4 | c2o 8459 | . . 3 class 2o | |
5 | 2, 1 | cop 4634 | . . 3 class ⟨𝑁, 𝑈⟩ |
6 | 4, 5 | cop 4634 | . 2 class ⟨2o, ⟨𝑁, 𝑈⟩⟩ |
7 | 3, 6 | wceq 1541 | 1 wff ∀𝑔𝑁𝑈 = ⟨2o, ⟨𝑁, 𝑈⟩⟩ |
Colors of variables: wff setvar class |
This definition is referenced by: goaleq12d 34337 gonanegoal 34338 sat1el2xp 34365 fmlaomn0 34376 goaln0 34379 goalrlem 34382 goalr 34383 fmla0disjsuc 34384 fmlasucdisj 34385 satffunlem1lem1 34388 satffunlem2lem1 34390 |
Copyright terms: Public domain | W3C validator |