This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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