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 ∈ suc ⁡ ω → Fmla ⁡ N = dom ⁡ ∅ Sat ∅ ⁡ N

Proof

Step Hyp Ref Expression
1 df-fmla ⊢ Fmla = n ∈ suc ⁡ ω ⟼ dom ⁡ ∅ Sat ∅ ⁡ n
2 1 a1i ⊢ N ∈ suc ⁡ ω → Fmla = n ∈ suc ⁡ ω ⟼ 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 ∈ suc ⁡ ω ∧ n = N → dom ⁡ ∅ Sat ∅ ⁡ n = dom ⁡ ∅ Sat ∅ ⁡ N
6 id ⊢ N ∈ suc ⁡ ω → N ∈ suc ⁡ ω
7 fvex ⊢ ∅ Sat ∅ ⁡ N ∈ V
8 7 dmex ⊢ dom ⁡ ∅ Sat ∅ ⁡ N ∈ V
9 8 a1i ⊢ N ∈ suc ⁡ ω → dom ⁡ ∅ Sat ∅ ⁡ N ∈ V
10 2 5 6 9 fvmptd ⊢ N ∈ suc ⁡ ω → Fmla ⁡ N = dom ⁡ ∅ Sat ∅ ⁡ N