This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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