Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fmla Structured version   Visualization version   GIF version

Definition df-fmla 34331
Description: Define the predicate which defines the set of valid Godel formulas. The parameter 𝑛 defines the maximum height of the formulas: the set (Fmlaβ€˜βˆ…) is all formulas of the form π‘₯ ∈ 𝑦 (which in our coding scheme is the set ({βˆ…} Γ— (Ο‰ Γ— Ο‰)); see df-sat 34329 for the full coding scheme), see fmla0 34368, and each extra level adds to the complexity of the formulas in (Fmlaβ€˜π‘›), see fmlasuc 34372. Remark: it is sufficient to have atomic formulas of the form π‘₯ ∈ 𝑦 only, because equations (formulas of the form π‘₯ = 𝑦), which are required as (atomic) formulas, can be introduced as a defined notion in terms of βˆˆπ‘”, see df-goeq 34430. (Fmlaβ€˜Ο‰) = βˆͺ 𝑛 ∈ Ο‰(Fmlaβ€˜π‘›) is the set of all valid formulas, see fmla 34367. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-fmla Fmla = (𝑛 ∈ suc Ο‰ ↦ dom ((βˆ… Sat βˆ…)β€˜π‘›))

Detailed syntax breakdown of Definition df-fmla
StepHypRef Expression
1 cfmla 34323 . 2 class Fmla
2 vn . . 3 setvar 𝑛
3 com 7854 . . . 4 class Ο‰
43csuc 6366 . . 3 class suc Ο‰
52cv 1540 . . . . 5 class 𝑛
6 c0 4322 . . . . . 6 class βˆ…
7 csat 34322 . . . . . 6 class Sat
86, 6, 7co 7408 . . . . 5 class (βˆ… Sat βˆ…)
95, 8cfv 6543 . . . 4 class ((βˆ… Sat βˆ…)β€˜π‘›)
109cdm 5676 . . 3 class dom ((βˆ… Sat βˆ…)β€˜π‘›)
112, 4, 10cmpt 5231 . 2 class (𝑛 ∈ suc Ο‰ ↦ dom ((βˆ… Sat βˆ…)β€˜π‘›))
121, 11wceq 1541 1 wff Fmla = (𝑛 ∈ suc Ο‰ ↦ dom ((βˆ… Sat βˆ…)β€˜π‘›))
Colors of variables: wff setvar class
This definition is referenced by:  fmlafv  34366  fmla  34367  fmlasuc0  34370
  Copyright terms: Public domain W3C validator