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 ∈ suc ⁡ ω ⟼ dom ⁡ ∅ Sat ∅ ⁡ n

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfmla class Fmla
1 vn setvar n
2 com class ω
3 2 csuc class suc ⁡ ω
4 c0 class ∅
5 csat class Sat
6 4 4 5 co class ∅ Sat ∅
7 1 cv setvar n
8 7 6 cfv class ∅ Sat ∅ ⁡ n
9 8 cdm class dom ⁡ ∅ Sat ∅ ⁡ n
10 1 3 9 cmpt class n ∈ suc ⁡ ω ⟼ dom ⁡ ∅ Sat ∅ ⁡ n
11 0 10 wceq wff Fmla = n ∈ suc ⁡ ω ⟼ dom ⁡ ∅ Sat ∅ ⁡ n