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

Metamath Proof Explorer

Theorem satfvel

Description: An element of the value of the satisfaction predicate as function over wff codes in the model M and the binary relation E on M at the code U for a wff using e. , -/\ , A. is a valuation S :om --> M of the variables (v0 = ( S(/) ) , v_1 = ( S1o ) , etc.) so that U is true under the assignment S . (Contributed by AV, 29-Oct-2023)

Ref Expression
Assertion satfvel 
|- ( ( ( M e. V /\ E e. W ) /\ U e. ( Fmla ` _om ) /\ S e. ( ( ( M Sat E ) ` _om ) ` U ) ) -> S : _om --> M )

Proof

Step Hyp Ref Expression
1 satfun 
 |-  ( ( M e. V /\ E e. W ) -> ( ( M Sat E ) ` _om ) : ( Fmla ` _om ) --> ~P ( M ^m _om ) )
2 ffvelcdm 
 |-  ( ( ( ( M Sat E ) ` _om ) : ( Fmla ` _om ) --> ~P ( M ^m _om ) /\ U e. ( Fmla ` _om ) ) -> ( ( ( M Sat E ) ` _om ) ` U ) e. ~P ( M ^m _om ) )
3 fvex 
 |-  ( ( ( M Sat E ) ` _om ) ` U ) e. _V
4 3 elpw 
 |-  ( ( ( ( M Sat E ) ` _om ) ` U ) e. ~P ( M ^m _om ) <-> ( ( ( M Sat E ) ` _om ) ` U ) C_ ( M ^m _om ) )
5 ssel 
 |-  ( ( ( ( M Sat E ) ` _om ) ` U ) C_ ( M ^m _om ) -> ( S e. ( ( ( M Sat E ) ` _om ) ` U ) -> S e. ( M ^m _om ) ) )
6 elmapi 
 |-  ( S e. ( M ^m _om ) -> S : _om --> M )
7 5 6 syl6 
 |-  ( ( ( ( M Sat E ) ` _om ) ` U ) C_ ( M ^m _om ) -> ( S e. ( ( ( M Sat E ) ` _om ) ` U ) -> S : _om --> M ) )
8 4 7 sylbi 
 |-  ( ( ( ( M Sat E ) ` _om ) ` U ) e. ~P ( M ^m _om ) -> ( S e. ( ( ( M Sat E ) ` _om ) ` U ) -> S : _om --> M ) )
9 2 8 syl 
 |-  ( ( ( ( M Sat E ) ` _om ) : ( Fmla ` _om ) --> ~P ( M ^m _om ) /\ U e. ( Fmla ` _om ) ) -> ( S e. ( ( ( M Sat E ) ` _om ) ` U ) -> S : _om --> M ) )
10 9 ex 
 |-  ( ( ( M Sat E ) ` _om ) : ( Fmla ` _om ) --> ~P ( M ^m _om ) -> ( U e. ( Fmla ` _om ) -> ( S e. ( ( ( M Sat E ) ` _om ) ` U ) -> S : _om --> M ) ) )
11 1 10 syl 
 |-  ( ( M e. V /\ E e. W ) -> ( U e. ( Fmla ` _om ) -> ( S e. ( ( ( M Sat E ) ` _om ) ` U ) -> S : _om --> M ) ) )
12 11 3imp 
 |-  ( ( ( M e. V /\ E e. W ) /\ U e. ( Fmla ` _om ) /\ S e. ( ( ( M Sat E ) ` _om ) ` U ) ) -> S : _om --> M )