Theorem fmlafv

Description: The valid Godel formulas of height N is the domain of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation at N . (Contributed by AV, 15-Sep-2023)

	Ref	Expression
Assertion	fmlafv	|- ( N e. suc _om -> ( Fmla ` N ) = dom ( ( (/) Sat (/) ) ` N ) )

Proof

Step	Hyp	Ref	Expression
1		df-fmla	|- Fmla = ( n e. suc _om |-> dom ( ( (/) Sat (/) ) ` n ) )
2	1	a1i	|- ( N e. suc _om -> Fmla = ( n e. suc _om |-> dom ( ( (/) Sat (/) ) ` n ) ) )
3		fveq2	|- ( n = N -> ( ( (/) Sat (/) ) ` n ) = ( ( (/) Sat (/) ) ` N ) )
4	3	dmeqd	|- ( n = N -> dom ( ( (/) Sat (/) ) ` n ) = dom ( ( (/) Sat (/) ) ` N ) )
5	4	adantl	|- ( ( N e. suc _om /\ n = N ) -> dom ( ( (/) Sat (/) ) ` n ) = dom ( ( (/) Sat (/) ) ` N ) )
6		id	|- ( N e. suc _om -> N e. suc _om )
7		fvex	|- ( ( (/) Sat (/) ) ` N ) e. _V
8	7	dmex	|- dom ( ( (/) Sat (/) ) ` N ) e. _V
9	8	a1i	|- ( N e. suc _om -> dom ( ( (/) Sat (/) ) ` N ) e. _V )
10	2 5 6 9	fvmptd	|- ( N e. suc _om -> ( Fmla ` N ) = dom ( ( (/) Sat (/) ) ` N ) )