This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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