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 = ( 𝑛 ∈ suc ω ↦ dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfmla Fmla
1 vn 𝑛
2 com ω
3 2 csuc suc ω
4 c0
5 csat Sat
6 4 4 5 co ( ∅ Sat ∅ )
7 1 cv 𝑛
8 7 6 cfv ( ( ∅ Sat ∅ ) ‘ 𝑛 )
9 8 cdm dom ( ( ∅ Sat ∅ ) ‘ 𝑛 )
10 1 3 9 cmpt ( 𝑛 ∈ suc ω ↦ dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) )
11 0 10 wceq Fmla = ( 𝑛 ∈ suc ω ↦ dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) )