---

Step * of Lemma sets_wf

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)].  (sets(C; X) ∈ small-category{[i | j']:l})
BY
{ (Auto
   THEN Unfold `sets` 0
   THEN (InstLemma `presheaf-elements_wf` [⌜parm{[i | j']}⌝]⋅ THEN BHyp -1)
   THEN Auto
   THEN Unfold `ps_context` 2
   THEN Fold `presheaf` 2) }

1
1. C : SmallCategory
2. X : presheaf{j':l}(C)
3. ∀C:small-category{[i | j']:l}. ∀P:presheaf{[i | j']:l}(C).  (el(P) ∈ small-category{[i | j']:l})
⊢ X ∈ presheaf{[i | j']:l}(C)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].    (sets(C;  X)  \mmember{}  small-category\{[i  |  j']:l\})


By

---

Latex:
(Auto
  THEN  Unfold  `sets`  0
  THEN  (InstLemma  `presheaf-elements\_wf`  [\mkleeneopen{}parm\{[i  |  j']\}\mkleeneclose{}]\mcdot{}  THEN  BHyp  -1)
  THEN  Auto
  THEN  Unfold  `ps\_context`  2
  THEN  Fold  `presheaf`  2)

---

Home Index