---

Step * of Lemma psc-restriction_wf

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[I,J:cat-ob(C)]. ∀[f:cat-arrow(C) J I]. ∀[s:X(I)].  (f(s) ∈ X(J))
BY
{ (ProveWfLemma THEN DContext 2 THEN Reduce 0 THEN All (RepUR ``I_set functor-ob``) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[I,J:cat-ob(C)].  \mforall{}[f:cat-arrow(C)  J  I].  \mforall{}[s:X(I)].
    (f(s)  \mmember{}  X(J))


By

---

Latex:
(ProveWfLemma  THEN  DContext  2  THEN  Reduce  0  THEN  All  (RepUR  ``I\_set  functor-ob``)  THEN  Auto)

---

Home Index