---

Step * of Lemma dM-lift-dMpair

∀[I,J:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[x,y:names(I)].  ((dM-lift(J;I;f) dMpair(x;y)) = f x ∧ f y ∈ Point(dM(J)))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma  `dMpair-eq-meet` [⌜I⌝;⌜x⌝;⌜y⌝]⋅
         THENA (Auto THEN OnMaybeHyp 4 (\h. Complete ((D h THEN Unhide THEN Auto))))
         )
   ) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. f : J ⟶ I
4. x : names(I)
5. y : names(I)
6. dMpair(x;y) = <x> ∧ <y> ∈ Point(dM(I))
⊢ (dM-lift(J;I;f) dMpair(x;y)) = f x ∧ f y ∈ Point(dM(J))

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].  \mforall{}[x,y:names(I)].    ((dM-lift(J;I;f)  dMpair(x;y))  =  f  x  \mwedge{}  f  y)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma    `dMpair-eq-meet`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  OnMaybeHyp  4  (\mbackslash{}h.  Complete  ((D  h  THEN  Unhide  THEN  Auto))))
              )
  )

---

Home Index