Theorem satfdmfmla

Description: The domain of the satisfaction predicate as function over wff codes in any model M and any binary relation E on M for a natural number N is the set of valid Godel formulas of height N . (Contributed by AV, 13-Oct-2023)

	Ref	Expression
Assertion	satfdmfmla	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = ( Fmla ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2	1 1	pm3.2i	⊢ ( ∅ ∈ V ∧ ∅ ∈ V )
3	2	jctr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( ∅ ∈ V ∧ ∅ ∈ V ) ) )
4	3	3adant3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( ∅ ∈ V ∧ ∅ ∈ V ) ) )
5		satfdm	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( ∅ ∈ V ∧ ∅ ∈ V ) ) → ∀ 𝑛 ∈ ω dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) )
6	4 5	syl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ∀ 𝑛 ∈ ω dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) )
7		fveq2	⊢ ( 𝑛 = 𝑁 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
8	7	dmeqd	⊢ ( 𝑛 = 𝑁 → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
9		fveq2	⊢ ( 𝑛 = 𝑁 → ( ( ∅ Sat ∅ ) ‘ 𝑛 ) = ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
10	9	dmeqd	⊢ ( 𝑛 = 𝑁 → dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
11	8 10	eqeq12d	⊢ ( 𝑛 = 𝑁 → ( dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) ↔ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
12	11	rspcv	⊢ ( 𝑁 ∈ ω → ( ∀ 𝑛 ∈ ω dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
13	12	3ad2ant3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ∀ 𝑛 ∈ ω dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑛 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑛 ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) ) )
14	6 13	mpd	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
15		elelsuc	⊢ ( 𝑁 ∈ ω → 𝑁 ∈ suc ω )
16	15	3ad2ant3	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → 𝑁 ∈ suc ω )
17		fmlafv	⊢ ( 𝑁 ∈ suc ω → ( Fmla ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
18	16 17	syl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( Fmla ‘ 𝑁 ) = dom ( ( ∅ Sat ∅ ) ‘ 𝑁 ) )
19	14 18	eqtr4d	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = ( Fmla ‘ 𝑁 ) )