---

Step * of Lemma presheaf-elements_wf

No Annotations
∀C:SmallCategory. ∀P:Presheaf(C).  (el(P) ∈ SmallCategory)
BY
{ (Auto THEN RepUR ``presheaf`` -1) }

1
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
⊢ el(P) ∈ SmallCategory

---

Latex:

---

Latex:
No  Annotations
\mforall{}C:SmallCategory.  \mforall{}P:Presheaf(C).    (el(P)  \mmember{}  SmallCategory)


By

---

Latex:
(Auto  THEN  RepUR  ``presheaf``  -1)

---

Home Index