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 ∈ V ∧ E ∈ W ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat E ⁡ ω ⁡ U → S : ω ⟶ M

Proof

Step Hyp Ref Expression
1 satfun ⊢ M ∈ V ∧ E ∈ W → M Sat E ⁡ ω : Fmla ⁡ ω ⟶ 𝒫 M ω
2 ffvelrn ⊢ M Sat E ⁡ ω : Fmla ⁡ ω ⟶ 𝒫 M ω ∧ U ∈ Fmla ⁡ ω → M Sat E ⁡ ω ⁡ U ∈ 𝒫 M ω
3 fvex ⊢ M Sat E ⁡ ω ⁡ U ∈ V
4 3 elpw ⊢ M Sat E ⁡ ω ⁡ U ∈ 𝒫 M ω ↔ M Sat E ⁡ ω ⁡ U ⊆ M ω
5 ssel ⊢ M Sat E ⁡ ω ⁡ U ⊆ M ω → S ∈ M Sat E ⁡ ω ⁡ U → S ∈ M ω
6 elmapi ⊢ S ∈ M ω → S : ω ⟶ M
7 5 6 syl6 ⊢ M Sat E ⁡ ω ⁡ U ⊆ M ω → S ∈ M Sat E ⁡ ω ⁡ U → S : ω ⟶ M
8 4 7 sylbi ⊢ M Sat E ⁡ ω ⁡ U ∈ 𝒫 M ω → S ∈ M Sat E ⁡ ω ⁡ U → S : ω ⟶ M
9 2 8 syl ⊢ M Sat E ⁡ ω : Fmla ⁡ ω ⟶ 𝒫 M ω ∧ U ∈ Fmla ⁡ ω → S ∈ M Sat E ⁡ ω ⁡ U → S : ω ⟶ M
10 9 ex ⊢ M Sat E ⁡ ω : Fmla ⁡ ω ⟶ 𝒫 M ω → U ∈ Fmla ⁡ ω → S ∈ M Sat E ⁡ ω ⁡ U → S : ω ⟶ M
11 1 10 syl ⊢ M ∈ V ∧ E ∈ W → U ∈ Fmla ⁡ ω → S ∈ M Sat E ⁡ ω ⁡ U → S : ω ⟶ M
12 11 3imp ⊢ M ∈ V ∧ E ∈ W ∧ U ∈ Fmla ⁡ ω ∧ S ∈ M Sat E ⁡ ω ⁡ U → S : ω ⟶ M