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 ∅ ) ‘ 𝑛 ) )