---

Step * of Lemma sub-presheaf-set_wf

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[P:I:cat-ob(C) ⟶ X(I) ⟶ ℙ{j'}].
  X | I,rho.P[I;rho] ∈ ps_context{j:l}(C) supposing psc-predicate(C; X; I,rho.P[I;rho])
BY
{ ProveWfLemma }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. P : I:cat-ob(C) ⟶ X(I) ⟶ ℙ{j'}
4. psc-predicate(C; X; I,rho.P[I;rho])
⊢ X|I,rho.P[I;rho] ∈ ps_context{j:l}(C)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[P:I:cat-ob(C)  {}\mrightarrow{}  X(I)  {}\mrightarrow{}  \mBbbP{}\{j'\}].
    X  |  I,rho.P[I;rho]  \mmember{}  ps\_context\{j:l\}(C)  supposing  psc-predicate(C;  X;  I,rho.P[I;rho])


By

---

Latex:
ProveWfLemma

---

Home Index