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