Theorem satff

Description: The satisfaction predicate as function over wff codes in the model M and the binary relation E on M . (Contributed by AV, 28-Oct-2023)

	Ref	Expression
Assertion	satff	|- ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( M Sat E ) ` N ) : ( Fmla ` N ) --> ~P ( M ^m _om ) )

Proof

Step	Hyp	Ref	Expression
1		satffun	|- ( ( M e. V /\ E e. W /\ N e. _om ) -> Fun ( ( M Sat E ) ` N ) )
2		satfdmfmla	|- ( ( M e. V /\ E e. W /\ N e. _om ) -> dom ( ( M Sat E ) ` N ) = ( Fmla ` N ) )
3		df-fn	|- ( ( ( M Sat E ) ` N ) Fn ( Fmla ` N ) <-> ( Fun ( ( M Sat E ) ` N ) /\ dom ( ( M Sat E ) ` N ) = ( Fmla ` N ) ) )
4	1 2 3	sylanbrc	|- ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( M Sat E ) ` N ) Fn ( Fmla ` N ) )
5		satfrnmapom	|- ( ( M e. V /\ E e. W /\ N e. _om ) -> ran ( ( M Sat E ) ` N ) C_ ~P ( M ^m _om ) )
6		df-f	|- ( ( ( M Sat E ) ` N ) : ( Fmla ` N ) --> ~P ( M ^m _om ) <-> ( ( ( M Sat E ) ` N ) Fn ( Fmla ` N ) /\ ran ( ( M Sat E ) ` N ) C_ ~P ( M ^m _om ) ) )
7	4 5 6	sylanbrc	|- ( ( M e. V /\ E e. W /\ N e. _om ) -> ( ( M Sat E ) ` N ) : ( Fmla ` N ) --> ~P ( M ^m _om ) )