---

Step * of Lemma dM-lift-is-id

∀[I:fset(ℕ)]. ∀[J:{J:fset(ℕ)| I ⊆ J} ]. ∀[h:I ⟶ J].
  ∀[x:Point(dM(I))]. ((dM-lift(I;J;h) x) = x ∈ Point(dM(I))) supposing ∀i:names(I). ((h i) = <i> ∈ Point(dM(I)))
BY
{ (RepeatFor 3 (Intro)
   THEN (Assert I ⊆ J BY
               (Unhide THEN Auto THEN Unfold `f-subset` 0 THEN Auto))
   THEN (Assert Point(dM(I)) ⊆r Point(dM(J)) BY
               Auto)
   THEN Auto
   THEN (InstLemma `dM-dma-hom-invariant` [⌜I⌝;⌜J⌝]⋅ THENA Auto)
   THEN BHyp -1 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[J:\{J:fset(\mBbbN{})|  I  \msubseteq{}  J\}  ].  \mforall{}[h:I  {}\mrightarrow{}  J].
    \mforall{}[x:Point(dM(I))].  ((dM-lift(I;J;h)  x)  =  x)  supposing  \mforall{}i:names(I).  ((h  i)  =  <i>)


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  (Assert  I  \msubseteq{}  J  BY
                          (Unhide  THEN  Auto  THEN  Unfold  `f-subset`  0  THEN  Auto))
  THEN  (Assert  Point(dM(I))  \msubseteq{}r  Point(dM(J))  BY
                          Auto)
  THEN  Auto
  THEN  (InstLemma  `dM-dma-hom-invariant`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index