Metamath Proof Explorer


Definition df-fmla

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 e. y (which in our coding scheme is the set ( { (/) } X. (om X. om ) ) ; see df-sat for the full coding scheme), see fmla0 , and each extra level adds to the complexity of the formulas in ( Fmlan ) , see fmlasuc . Remark: it is sufficient to have atomic formulas of the form x e. y only, because equations (formulas of the form x = y ), which are required as (atomic) formulas, can be introduced as a defined notion in terms of e.g , see df-goeq . ( Fmla_om ) = U_ n e. _om ( Fmlan ) is the set of all valid formulas, see fmla . (Contributed by Mario Carneiro, 14-Jul-2013)

Ref Expression
Assertion df-fmla
|- Fmla = ( n e. suc _om |-> dom ( ( (/) Sat (/) ) ` n ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfmla
 |-  Fmla
1 vn
 |-  n
2 com
 |-  _om
3 2 csuc
 |-  suc _om
4 c0
 |-  (/)
5 csat
 |-  Sat
6 4 4 5 co
 |-  ( (/) Sat (/) )
7 1 cv
 |-  n
8 7 6 cfv
 |-  ( ( (/) Sat (/) ) ` n )
9 8 cdm
 |-  dom ( ( (/) Sat (/) ) ` n )
10 1 3 9 cmpt
 |-  ( n e. suc _om |-> dom ( ( (/) Sat (/) ) ` n ) )
11 0 10 wceq
 |-  Fmla = ( n e. suc _om |-> dom ( ( (/) Sat (/) ) ` n ) )