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⁡MSatE⁡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⁡MSatE⁡n=dom⁡∅Sat∅⁡n
6 4 5 syl ⊢M∈V∧E∈W∧N∈ω→∀n∈ωdom⁡MSatE⁡n=dom⁡∅Sat∅⁡n
7 fveq2 ⊢n=N→MSatE⁡n=MSatE⁡N
8 7 dmeqd ⊢n=N→dom⁡MSatE⁡n=dom⁡MSatE⁡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⁡MSatE⁡n=dom⁡∅Sat∅⁡n↔dom⁡MSatE⁡N=dom⁡∅Sat∅⁡N
12 11 rspcv ⊢N∈ω→∀n∈ωdom⁡MSatE⁡n=dom⁡∅Sat∅⁡n→dom⁡MSatE⁡N=dom⁡∅Sat∅⁡N
13 12 3ad2ant3 ⊢M∈V∧E∈W∧N∈ω→∀n∈ωdom⁡MSatE⁡n=dom⁡∅Sat∅⁡n→dom⁡MSatE⁡N=dom⁡∅Sat∅⁡N
14 6 13 mpd ⊢M∈V∧E∈W∧N∈ω→dom⁡MSatE⁡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⁡MSatE⁡N=Fmla⁡N