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 ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑈 ∈ ( Fmla ‘ ω ) ∧ 𝑆 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) ) → 𝑆 : ω ⟶ 𝑀 )

Proof

Step Hyp Ref Expression
1 satfun ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ ω ) : ( Fmla ‘ ω ) ⟶ 𝒫 ( 𝑀 ↑m ω ) )
2 ffvelcdm ⊢ ( ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) : ( Fmla ‘ ω ) ⟶ 𝒫 ( 𝑀 ↑m ω ) ∧ 𝑈 ∈ ( Fmla ‘ ω ) ) → ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) ∈ 𝒫 ( 𝑀 ↑m ω ) )
3 fvex ⊢ ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) ∈ V
4 3 elpw ⊢ ( ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) ∈ 𝒫 ( 𝑀 ↑m ω ) ↔ ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) ⊆ ( 𝑀 ↑m ω ) )
5 ssel ⊢ ( ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) ⊆ ( 𝑀 ↑m ω ) → ( 𝑆 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) → 𝑆 ∈ ( 𝑀 ↑m ω ) ) )
6 elmapi ⊢ ( 𝑆 ∈ ( 𝑀 ↑m ω ) → 𝑆 : ω ⟶ 𝑀 )
7 5 6 syl6 ⊢ ( ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) ⊆ ( 𝑀 ↑m ω ) → ( 𝑆 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) → 𝑆 : ω ⟶ 𝑀 ) )
8 4 7 sylbi ⊢ ( ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) ∈ 𝒫 ( 𝑀 ↑m ω ) → ( 𝑆 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) → 𝑆 : ω ⟶ 𝑀 ) )
9 2 8 syl ⊢ ( ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) : ( Fmla ‘ ω ) ⟶ 𝒫 ( 𝑀 ↑m ω ) ∧ 𝑈 ∈ ( Fmla ‘ ω ) ) → ( 𝑆 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) → 𝑆 : ω ⟶ 𝑀 ) )
10 9 ex ⊢ ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) : ( Fmla ‘ ω ) ⟶ 𝒫 ( 𝑀 ↑m ω ) → ( 𝑈 ∈ ( Fmla ‘ ω ) → ( 𝑆 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) → 𝑆 : ω ⟶ 𝑀 ) ) )
11 1 10 syl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑈 ∈ ( Fmla ‘ ω ) → ( 𝑆 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) → 𝑆 : ω ⟶ 𝑀 ) ) )
12 11 3imp ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑈 ∈ ( Fmla ‘ ω ) ∧ 𝑆 ∈ ( ( ( 𝑀 Sat 𝐸 ) ‘ ω ) ‘ 𝑈 ) ) → 𝑆 : ω ⟶ 𝑀 )