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 ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ ω → dom ⁡ M Sat E ⁡ N = Fmla ⁡ N

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 1 1 pm3.2i ⊢ ∅ ∈ V ∧ ∅ ∈ V
3 2 jctr ⊢ M ∈ V ∧ E ∈ W → M ∈ V ∧ E ∈ W ∧ ∅ ∈ V ∧ ∅ ∈ V
4 3 3adant3 ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ ω → M ∈ V ∧ E ∈ W ∧ ∅ ∈ V ∧ ∅ ∈ V
5 satfdm ⊢ M ∈ V ∧ E ∈ W ∧ ∅ ∈ V ∧ ∅ ∈ V → ∀ n ∈ ω dom ⁡ M Sat E ⁡ n = dom ⁡ ∅ Sat ∅ ⁡ n
6 4 5 syl ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ ω → ∀ n ∈ ω dom ⁡ M Sat E ⁡ n = dom ⁡ ∅ Sat ∅ ⁡ n
7 fveq2 ⊢ n = N → M Sat E ⁡ n = M Sat E ⁡ N
8 7 dmeqd ⊢ n = N → dom ⁡ M Sat E ⁡ n = dom ⁡ M Sat E ⁡ N
9 fveq2 ⊢ n = N → ∅ Sat ∅ ⁡ n = ∅ Sat ∅ ⁡ N
10 9 dmeqd ⊢ n = N → dom ⁡ ∅ Sat ∅ ⁡ n = dom ⁡ ∅ Sat ∅ ⁡ N
11 8 10 eqeq12d ⊢ n = N → dom ⁡ M Sat E ⁡ n = dom ⁡ ∅ Sat ∅ ⁡ n ↔ dom ⁡ M Sat E ⁡ N = dom ⁡ ∅ Sat ∅ ⁡ N
12 11 rspcv ⊢ N ∈ ω → ∀ n ∈ ω dom ⁡ M Sat E ⁡ n = dom ⁡ ∅ Sat ∅ ⁡ n → dom ⁡ M Sat E ⁡ N = dom ⁡ ∅ Sat ∅ ⁡ N
13 12 3ad2ant3 ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ ω → ∀ n ∈ ω dom ⁡ M Sat E ⁡ n = dom ⁡ ∅ Sat ∅ ⁡ n → dom ⁡ M Sat E ⁡ N = dom ⁡ ∅ Sat ∅ ⁡ N
14 6 13 mpd ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ ω → dom ⁡ M Sat E ⁡ N = dom ⁡ ∅ Sat ∅ ⁡ N
15 elelsuc ⊢ N ∈ ω → N ∈ suc ⁡ ω
16 15 3ad2ant3 ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ ω → N ∈ suc ⁡ ω
17 fmlafv ⊢ N ∈ suc ⁡ ω → Fmla ⁡ N = dom ⁡ ∅ Sat ∅ ⁡ N
18 16 17 syl ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ ω → Fmla ⁡ N = dom ⁡ ∅ Sat ∅ ⁡ N
19 14 18 eqtr4d ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ ω → dom ⁡ M Sat E ⁡ N = Fmla ⁡ N