---

Step * of Lemma dM-lift_wf

∀[I,J:fset(ℕ)]. ∀[f:I ⟶ J].  (dM-lift(I;J;f) ∈ {g:dma-hom(dM(J);dM(I))| ∀j:names(J). ((g <j>) = (f j) ∈ Point(dM(I)))} \000C)
BY
{ (Auto THEN Unfold `names-hom` -1) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. f : names(J) ⟶ Point(dM(I))
⊢ dM-lift(I;J;f) ∈ {g:dma-hom(dM(J);dM(I))| ∀j:names(J). ((g <j>) = (f j) ∈ Point(dM(I)))} 

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[f:I  {}\mrightarrow{}  J].
    (dM-lift(I;J;f)  \mmember{}  \{g:dma-hom(dM(J);dM(I))|  \mforall{}j:names(J).  ((g  <j>)  =  (f  j))\}  )


By

---

Latex:
(Auto  THEN  Unfold  `names-hom`  -1)

---

Home Index