---

Step * of Lemma sets-ob

∀[C:SmallCategory]. ∀[X:Top].  (cat-ob(sets(C; X)) ~ I:cat-ob(C) × X(I))
BY
{ ((Auto THEN (Assert C ∈ SmallCategory BY Trivial))
   THEN DCat 1
   THEN RepUR ``sets presheaf-elements mk-cat I_set`` 0
   THEN RWO "cat_ob_op_lemma" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[X:Top].    (cat-ob(sets(C;  X))  \msim{}  I:cat-ob(C)  \mtimes{}  X(I))


By

---

Latex:
((Auto  THEN  (Assert  C  \mmember{}  SmallCategory  BY  Trivial))
  THEN  DCat  1
  THEN  RepUR  ``sets  presheaf-elements  mk-cat  I\_set``  0
  THEN  RWO  "cat\_ob\_op\_lemma"  0
  THEN  Auto)

---

Home Index