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

Definition df-fmla 23943
Description: Define the predicate which defines the set of valid Godel formulas. The parameter  n defines the maximum height of the formulas: the set  ( Fmla `  (/) ) is all formulas of the form  x  =  y or  x  e.  y (which in our coding scheme is the set  ( { (/) ,  1o }  X.  ( om  X.  om ) ); see df-sat 23941 for the full coding scheme), and each extra level adds to the complexity of the formulas in  ( Fmla `  n
).  ( Fmla `  om )  =  U_ n  e. 
om ( Fmla `  n
) is the set of all valid formulas. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-fmla  |-  Fmla  =  ( n  e.  suc  om 
|->  dom  ( ( (/)  Sat  (/) ) `  n ) )

Detailed syntax breakdown of Definition df-fmla
StepHypRef Expression
1 cfmla 23935 . 2  class  Fmla
2 vn . . 3  set  n
3 com 4672 . . . 4  class  om
43csuc 4410 . . 3  class  suc  om
52cv 1631 . . . . 5  class  n
6 c0 3468 . . . . . 6  class  (/)
7 csat 23934 . . . . . 6  class  Sat
86, 6, 7co 5874 . . . . 5  class  ( (/)  Sat  (/) )
95, 8cfv 5271 . . . 4  class  ( (
(/)  Sat  (/) ) `  n
)
109cdm 4705 . . 3  class  dom  (
( (/)  Sat  (/) ) `  n )
112, 4, 10cmpt 4093 . 2  class  ( n  e.  suc  om  |->  dom  ( ( (/)  Sat  (/) ) `  n ) )
121, 11wceq 1632 1  wff  Fmla  =  ( n  e.  suc  om 
|->  dom  ( ( (/)  Sat  (/) ) `  n ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator