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 \in suc ω \to Fmla (N) = dom (\emptyset Sat \emptyset) (N)$

Proof

Step	Hyp	Ref	Expression
1		df-fmla	$⊢ Fmla = (n \in suc ω ⟼ dom (\emptyset Sat \emptyset) (n))$
2	1	a1i	$⊢ N \in suc ω \to Fmla = (n \in suc ω ⟼ dom (\emptyset Sat \emptyset) (n))$
3		fveq2	$⊢ n = N \to (\emptyset Sat \emptyset) (n) = (\emptyset Sat \emptyset) (N)$
4	3	dmeqd	$⊢ n = N \to dom (\emptyset Sat \emptyset) (n) = dom (\emptyset Sat \emptyset) (N)$
5	4	adantl	$⊢ (N \in suc ω \land n = N) \to dom (\emptyset Sat \emptyset) (n) = dom (\emptyset Sat \emptyset) (N)$
6		id	$⊢ N \in suc ω \to N \in suc ω$
7		fvex	$⊢ (\emptyset Sat \emptyset) (N) \in V$
8	7	dmex	$⊢ dom (\emptyset Sat \emptyset) (N) \in V$
9	8	a1i	$⊢ N \in suc ω \to dom (\emptyset Sat \emptyset) (N) \in V$
10	2 5 6 9	fvmptd	$⊢ N \in suc ω \to Fmla (N) = dom (\emptyset Sat \emptyset) (N)$