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	$$⊢\mathrm{Fmla}=\left(n\in \mathrm{suc}\mathrm{\omega }⟼\mathrm{dom}\left(\varnothing \mathrm{Sat}\varnothing \right)\left(n\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfmla	$$class\mathrm{Fmla}$$
1		vn	$$setvarn$$
2		com	$$class\mathrm{\omega }$$
3	2	csuc	$$class\mathrm{suc}\mathrm{\omega }$$
4		c0	$$class\varnothing$$
5		csat	$$class\mathrm{Sat}$$
6	4 4 5	co	$$class\left(\varnothing \mathrm{Sat}\varnothing \right)$$
7	1	cv	$$setvarn$$
8	7 6	cfv	$$class\left(\varnothing \mathrm{Sat}\varnothing \right)\left(n\right)$$
9	8	cdm	$$class\mathrm{dom}\left(\varnothing \mathrm{Sat}\varnothing \right)\left(n\right)$$
10	1 3 9	cmpt	$$class\left(n\in \mathrm{suc}\mathrm{\omega }⟼\mathrm{dom}\left(\varnothing \mathrm{Sat}\varnothing \right)\left(n\right)\right)$$
11	0 10	wceq	$$wff\mathrm{Fmla}=\left(n\in \mathrm{suc}\mathrm{\omega }⟼\mathrm{dom}\left(\varnothing \mathrm{Sat}\varnothing \right)\left(n\right)\right)$$