Definition df-fmla 31327

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 = y or x e. y (which in our coding scheme is the set ( { (/) , 1o } X. ( om X. om ) ); see df-sat 31325 for the full coding scheme), and each extra level adds to the complexity of the formulas in ( Fmla ` n ). ( Fmla ` om ) = U_ n e. om ( Fmla ` n ) is the set of all valid formulas. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-fmla	|- Fmla = ( n e. suc om |-> dom ( ( (/) Sat (/) ) ` n ) )

Detailed syntax breakdown of Definition df-fmla

Step	Hyp	Ref	Expression
1		cfmla 31319	. 2 class Fmla
2		vn	. . 3 setvar n
3		com 7065	. . . 4 class om
4	3	csuc 5725	. . 3 class suc om
5	2	cv 1482	. . . . 5 class n
6		c0 3915	. . . . . 6 class (/)
7		csat 31318	. . . . . 6 class Sat
8	6, 6, 7	co 6650	. . . . 5 class ( (/) Sat (/) )
9	5, 8	cfv 5888	. . . 4 class ( ( (/) Sat (/) ) ` n )
10	9	cdm 5114	. . 3 class dom ( ( (/) Sat (/) ) ` n )
11	2, 4, 10	cmpt 4729	. 2 class ( n e. suc om |-> dom ( ( (/) Sat (/) ) ` n ) )
12	1, 11	wceq 1483	1 wff Fmla = ( n e. suc om |-> dom ( ( (/) Sat (/) ) ` n ) )

This definition is referenced by: (None)