Metamath Proof Explorer


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 ω ) )