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 e. V /\ E e. W /\ N e. _om ) -> dom ( ( M Sat E ) ` N ) = ( Fmla ` N ) )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 1 1 pm3.2i 
 |-  ( (/) e. _V /\ (/) e. _V )
3 2 jctr 
 |-  ( ( M e. V /\ E e. W ) -> ( ( M e. V /\ E e. W ) /\ ( (/) e. _V /\ (/) e. _V ) ) )
4 3 3adant3 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( M e. V /\ E e. W ) /\ ( (/) e. _V /\ (/) e. _V ) ) )
5 satfdm 
 |-  ( ( ( M e. V /\ E e. W ) /\ ( (/) e. _V /\ (/) e. _V ) ) -> A. n e. _om dom ( ( M Sat E ) ` n ) = dom ( ( (/) Sat (/) ) ` n ) )
6 4 5 syl 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> A. n e. _om 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 e. _om -> ( A. n e. _om dom ( ( M Sat E ) ` n ) = dom ( ( (/) Sat (/) ) ` n ) -> dom ( ( M Sat E ) ` N ) = dom ( ( (/) Sat (/) ) ` N ) ) )
13 12 3ad2ant3 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( A. n e. _om dom ( ( M Sat E ) ` n ) = dom ( ( (/) Sat (/) ) ` n ) -> dom ( ( M Sat E ) ` N ) = dom ( ( (/) Sat (/) ) ` N ) ) )
14 6 13 mpd 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> dom ( ( M Sat E ) ` N ) = dom ( ( (/) Sat (/) ) ` N ) )
15 elelsuc 
 |-  ( N e. _om -> N e. suc _om )
16 15 3ad2ant3 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> N e. suc _om )
17 fmlafv 
 |-  ( N e. suc _om -> ( Fmla ` N ) = dom ( ( (/) Sat (/) ) ` N ) )
18 16 17 syl 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( Fmla ` N ) = dom ( ( (/) Sat (/) ) ` N ) )
19 14 18 eqtr4d 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> dom ( ( M Sat E ) ` N ) = ( Fmla ` N ) )