Metamath Proof Explorer


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