Theorem satff

Description: The satisfaction predicate as function over wff codes in the model M and the binary relation E on M . (Contributed by AV, 28-Oct-2023)

	Ref	Expression
Assertion	satff	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) : ( Fmla ‘ 𝑁 ) ⟶ 𝒫 ( 𝑀 ↑m ω ) )

Proof

Step	Hyp	Ref	Expression
1		satffun	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
2		satfdmfmla	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = ( Fmla ‘ 𝑁 ) )
3		df-fn	⊢ ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) Fn ( Fmla ‘ 𝑁 ) ↔ ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ∧ dom ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = ( Fmla ‘ 𝑁 ) ) )
4	1 2 3	sylanbrc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) Fn ( Fmla ‘ 𝑁 ) )
5		satfrnmapom	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ 𝒫 ( 𝑀 ↑m ω ) )
6		df-f	⊢ ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) : ( Fmla ‘ 𝑁 ) ⟶ 𝒫 ( 𝑀 ↑m ω ) ↔ ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) Fn ( Fmla ‘ 𝑁 ) ∧ ran ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ⊆ 𝒫 ( 𝑀 ↑m ω ) ) )
7	4 5 6	sylanbrc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) : ( Fmla ‘ 𝑁 ) ⟶ 𝒫 ( 𝑀 ↑m ω ) )