---

Step * 1 of Lemma dM-subobject


1. I : fset(ℕ)
2. J : fset(ℕ)
3. I ⊆ J
⊢ λv.v ∈ Hom(dM(I);dM(J))
BY
{ (RepeatFor 2 ((MemTypeCD THEN Reduce 0 THEN Auto))
   THEN (\p. let T,x,y = dest_equal (concl p) in Subst (mk_sqequal_term x y) 0 p THENM Auto)
   THEN (RepUR ``dM free-DeMorgan-algebra lattice-meet lattice-join`` 0
         THEN RepUR `` mk-DeMorgan-algebra free-DeMorgan-lattice`` 0
         )
   THEN RepUR ``free-dist-lattice mk-bounded-distributive-lattice mk-bounded-lattice`` 0
   THEN RepUR ``union-deq`` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  fset(\mBbbN{})
3.  I  \msubseteq{}  J
\mvdash{}  \mlambda{}v.v  \mmember{}  Hom(dM(I);dM(J))


By

---

Latex:
(RepeatFor  2  ((MemTypeCD  THEN  Reduce  0  THEN  Auto))
  THEN  (\mbackslash{}p.  let  T,x,y  =  dest\_equal  (concl  p)  in  Subst  (mk\_sqequal\_term  x  y)  0  p  THENM  Auto)
  THEN  (RepUR  ``dM  free-DeMorgan-algebra  lattice-meet  lattice-join``  0
              THEN  RepUR  ``  mk-DeMorgan-algebra  free-DeMorgan-lattice``  0
              )
  THEN  RepUR  ``free-dist-lattice  mk-bounded-distributive-lattice  mk-bounded-lattice``  0
  THEN  RepUR  ``union-deq``  0
  THEN  Auto)

---

Home Index