This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )