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 \in V \land E \in W) \land U \in Fmla (ω) \land S \in (M Sat E) (ω) (U)) \to S : ω ⟶ M$

Proof

Step	Hyp	Ref	Expression
1		satfun	$⊢ (M \in V \land E \in W) \to (M Sat E) (ω) : Fmla (ω) ⟶ 𝒫 (M^{ω})$
2		ffvelcdm	$⊢ ((M Sat E) (ω) : Fmla (ω) ⟶ 𝒫 (M^{ω}) \land U \in Fmla (ω)) \to (M Sat E) (ω) (U) \in 𝒫 (M^{ω})$
3		fvex	$⊢ (M Sat E) (ω) (U) \in V$
4	3	elpw	$⊢ (M Sat E) (ω) (U) \in 𝒫 (M^{ω}) \leftrightarrow (M Sat E) (ω) (U) \subseteq M^{ω}$
5		ssel	$⊢ (M Sat E) (ω) (U) \subseteq M^{ω} \to (S \in (M Sat E) (ω) (U) \to S \in (M^{ω}))$
6		elmapi	$⊢ S \in (M^{ω}) \to S : ω ⟶ M$
7	5 6	syl6	$⊢ (M Sat E) (ω) (U) \subseteq M^{ω} \to (S \in (M Sat E) (ω) (U) \to S : ω ⟶ M)$
8	4 7	sylbi	$⊢ (M Sat E) (ω) (U) \in 𝒫 (M^{ω}) \to (S \in (M Sat E) (ω) (U) \to S : ω ⟶ M)$
9	2 8	syl	$⊢ ((M Sat E) (ω) : Fmla (ω) ⟶ 𝒫 (M^{ω}) \land U \in Fmla (ω)) \to (S \in (M Sat E) (ω) (U) \to S : ω ⟶ M)$
10	9	ex	$⊢ (M Sat E) (ω) : Fmla (ω) ⟶ 𝒫 (M^{ω}) \to (U \in Fmla (ω) \to (S \in (M Sat E) (ω) (U) \to S : ω ⟶ M))$
11	1 10	syl	$⊢ (M \in V \land E \in W) \to (U \in Fmla (ω) \to (S \in (M Sat E) (ω) (U) \to S : ω ⟶ M))$
12	11	3imp	$⊢ ((M \in V \land E \in W) \land U \in Fmla (ω) \land S \in (M Sat E) (ω) (U)) \to S : ω ⟶ M$

Metamath Proof Explorer

Theorem satfvel

Proof