---

Step * 1 of Lemma dM-lift-is-id2


1. I : fset(ℕ)
2. J : {J:fset(ℕ)| I ⊆ J} 
3. K : {K:fset(ℕ)| I ⊆ K} 
4. h : K ⟶ J
5. ∀i:names(I). ((h i) = <i> ∈ Point(dM(K)))
6. x : Point(dM(I))
7. dM-lift(K;J;h) o (λv.v) ∈ dma-hom(dM(I);dM(K))
8. (dM-lift(K;J;h) o (λv.v)) = (λv.v) ∈ (Point(dM(I)) ⟶ Point(dM(K)))
⊢ (dM-lift(K;J;h) x) = x ∈ Point(dM(K))
BY
{ ((ApFunToHypEquands `Z' ⌜Z x⌝ ⌜Point(dM(K))⌝ (-1)⋅ THENA Auto) THEN RepUR ``compose`` -1 THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  \{J:fset(\mBbbN{})|  I  \msubseteq{}  J\} 
3.  K  :  \{K:fset(\mBbbN{})|  I  \msubseteq{}  K\} 
4.  h  :  K  {}\mrightarrow{}  J
5.  \mforall{}i:names(I).  ((h  i)  =  <i>)
6.  x  :  Point(dM(I))
7.  dM-lift(K;J;h)  o  (\mlambda{}v.v)  \mmember{}  dma-hom(dM(I);dM(K))
8.  (dM-lift(K;J;h)  o  (\mlambda{}v.v))  =  (\mlambda{}v.v)
\mvdash{}  (dM-lift(K;J;h)  x)  =  x


By

---

Latex:
((ApFunToHypEquands  `Z'  \mkleeneopen{}Z  x\mkleeneclose{}  \mkleeneopen{}Point(dM(K))\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)  THEN  RepUR  ``compose``  -1  THEN  Auto)

---

Home Index