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		ffvelrn	⊢ ( ( ( ( 𝑀 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 𝐸 ) ‘ ω ) ‘ 𝑈 ) ) → 𝑆 : ω ⟶ 𝑀 )