---

Step * of Lemma presheaf-subset_wf1

No Annotations
∀[C:SmallCategory]. ∀[F:presheaf{j:l}(C)]. ∀[P:I:cat-ob(C) ⟶ (F I) ⟶ ℙ{j}].
  F|I,rho.P[I;rho] ∈ presheaf{j:l}(C) supposing stable-element-predicate(C;F;I,rho.P[I;rho])
BY
{ ((InstLemma `presheaf_wf1` [] THEN ParallelLast')
   THEN (InstLemma `stable-element-predicate_wf1` [⌜C⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN Thin (-2)
   THEN Unfold `presheaf-subset` 0
   THEN (MemCD THENA Auto)
   THEN ((D 0 THENA Auto) ORELSE Auto)
   THEN Intros
   THEN Thin 2) }

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

2
1. C : SmallCategory
2. F : presheaf{j:l}(C)
3. P : I:cat-ob(C) ⟶ (F I) ⟶ ℙ{j}
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:F I| P[I;rho]} 
⊢ (F I K (cat-comp(C) K J I g f) rho) = (F J K g (F I J f rho)) ∈ {rho:F K| P[K;rho]} 

---

Latex:

---

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


By

---

Latex:
((InstLemma  `presheaf\_wf1`  []  THEN  ParallelLast')
  THEN  (InstLemma  `stable-element-predicate\_wf1`  [\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  Thin  (-2)
  THEN  Unfold  `presheaf-subset`  0
  THEN  (MemCD  THENA  Auto)
  THEN  ((D  0  THENA  Auto)  ORELSE  Auto)
  THEN  Intros
  THEN  Thin  2)

---

Home Index