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

Proof

Step Hyp Ref Expression
1 satffun ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ ω → Fun ⁡ M Sat E ⁡ N
2 satfdmfmla ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ ω → dom ⁡ M Sat E ⁡ N = Fmla ⁡ N
3 df-fn ⊢ M Sat E ⁡ N Fn Fmla ⁡ N ↔ Fun ⁡ M Sat E ⁡ N ∧ dom ⁡ M Sat E ⁡ N = Fmla ⁡ N
4 1 2 3 sylanbrc ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ ω → M Sat E ⁡ N Fn Fmla ⁡ N
5 satfrnmapom ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ ω → ran ⁡ M Sat E ⁡ N ⊆ 𝒫 M ω
6 df-f ⊢ M Sat E ⁡ N : Fmla ⁡ N ⟶ 𝒫 M ω ↔ M Sat E ⁡ N Fn Fmla ⁡ N ∧ ran ⁡ M Sat E ⁡ N ⊆ 𝒫 M ω
7 4 5 6 sylanbrc ⊢ M ∈ V ∧ E ∈ W ∧ N ∈ ω → M Sat E ⁡ N : Fmla ⁡ N ⟶ 𝒫 M ω