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