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