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	⊢ ( 𝑁 ∈ suc ω → ( Fmla ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		df-fmla	⊢ Fmla = ( 𝑛 ∈ suc ω ↦ dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) )
2	1	a1i	⊢ ( 𝑁 ∈ suc ω → Fmla = ( 𝑛 ∈ suc ω ↦ dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) ) )
3		fveq2	⊢ ( 𝑛 = 𝑁 → ( ( ∅ Sat ∅ ) ‘ 𝑛 ) = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
4	3	dmeqd	⊢ ( 𝑛 = 𝑁 → dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
5	4	adantl	⊢ ( ( 𝑁 ∈ suc ω ∧ 𝑛 = 𝑁 ) → dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
6		id	⊢ ( 𝑁 ∈ suc ω → 𝑁 ∈ suc ω )
7		fvex	⊢ ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∈ V
8	7	dmex	⊢ dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∈ V
9	8	a1i	⊢ ( 𝑁 ∈ suc ω → dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ∈ V )
10	2 5 6 9	fvmptd	⊢ ( 𝑁 ∈ suc ω → ( Fmla ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )

Metamath Proof Explorer

Theorem fmlafv

Proof