Definition df-fmla 35372

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 35370 for the full coding scheme), see fmla0 35409, and each extra level adds to the complexity of the formulas in (Fmla‘𝑛), see fmlasuc 35413. 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 35471. (Fmla‘ω) = ∪ 𝑛 ∈ ω(Fmla‘𝑛) is the set of all valid formulas, see fmla 35408. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-fmla	⊢ Fmla = (𝑛 ∈ suc ω ↦ dom ((∅ Sat ∅)‘𝑛))

Detailed syntax breakdown of Definition df-fmla

Step	Hyp	Ref	Expression
1		cfmla 35364	. 2 class Fmla
2		vn	. . 3 setvar 𝑛
3		com 7866	. . . 4 class ω
4	3	csuc 6359	. . 3 class suc ω
5	2	cv 1539	. . . . 5 class 𝑛
6		c0 4313	. . . . . 6 class ∅
7		csat 35363	. . . . . 6 class Sat
8	6, 6, 7	co 7410	. . . . 5 class (∅ Sat ∅)
9	5, 8	cfv 6536	. . . 4 class ((∅ Sat ∅)‘𝑛)
10	9	cdm 5659	. . 3 class dom ((∅ Sat ∅)‘𝑛)
11	2, 4, 10	cmpt 5206	. 2 class (𝑛 ∈ suc ω ↦ dom ((∅ Sat ∅)‘𝑛))
12	1, 11	wceq 1540	1 wff Fmla = (𝑛 ∈ suc ω ↦ dom ((∅ Sat ∅)‘𝑛))

This definition is referenced by:  fmlafv  35407  fmla  35408  fmlasuc0  35411