---

Step * of Lemma presheaf-subset_wf

∀[C:SmallCategory]. ∀[F:Presheaf(C)]. ∀[P:I:cat-ob(C) ⟶ (ob(F) I) ⟶ ℙ].
  F|I,rho.P[I;rho] ∈ Presheaf(C) supposing stable-element-predicate(C;F;I,rho.P[I;rho])
BY
{ ProveWfLemma }

1
1. C : SmallCategory
2. F : Presheaf(C)
3. P : I:cat-ob(C) ⟶ (ob(F) I) ⟶ ℙ
4. stable-element-predicate(C;F;I,rho.P[I;rho])
5. I : cat-ob(C)
6. rho : {rho:ob(F) I| P[I;rho]} 
⊢ (arrow(F) I I (cat-id(C) I) rho) = rho ∈ {rho:ob(F) I| P[I;rho]} 

2
1. C : SmallCategory
2. F : Presheaf(C)
3. P : I:cat-ob(C) ⟶ (ob(F) I) ⟶ ℙ
4. stable-element-predicate(C;F;I,rho.P[I;rho])
5. I : cat-ob(C)
6. J : cat-ob(C)
7. K : cat-ob(C)
8. f : cat-arrow(C) J I
9. g : cat-arrow(C) K J
10. rho : {rho:ob(F) I| P[I;rho]} 
⊢ (arrow(F) I K (cat-comp(C) K J I g f) rho) = (arrow(F) J K g (arrow(F) I J f rho)) ∈ {rho:ob(F) K| P[K;rho]} 

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[F:Presheaf(C)].  \mforall{}[P:I:cat-ob(C)  {}\mrightarrow{}  (ob(F)  I)  {}\mrightarrow{}  \mBbbP{}].
    F|I,rho.P[I;rho]  \mmember{}  Presheaf(C)  supposing  stable-element-predicate(C;F;I,rho.P[I;rho])


By

---

Latex:
ProveWfLemma

---

Home Index