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