---

Step * 2 1 of Lemma presheaf-element-map_wf


1. C : SmallCategory
2. A : Presheaf(C)
3. B : Presheaf(C)
4. m : A ⟶ B
5. A@0 : cat-ob(op-cat(C))
6. x1 : ob(A) A@0
7. A1 : cat-ob(op-cat(C))
8. y1 : ob(A) A1
9. x : {f:cat-arrow(op-cat(C)) A1 A@0| (arrow(A) A1 A@0 f y1) = x1 ∈ (ob(A) A@0)} 
⊢ x ∈ {f:cat-arrow(op-cat(C)) A1 A@0| (arrow(B) A1 A@0 f (m A1 y1)) = (m A@0 x1) ∈ (ob(B) A@0)} 
BY
{ (D -1 THEN At ⌜Type⌝ MemTypeCD⋅ THEN Auto) }

1
.....set predicate..... 
1. C : SmallCategory
2. A : Presheaf(C)
3. B : Presheaf(C)
4. m : A ⟶ B
5. A@0 : cat-ob(op-cat(C))
6. x1 : ob(A) A@0
7. A1 : cat-ob(op-cat(C))
8. y1 : ob(A) A1
9. x : cat-arrow(op-cat(C)) A1 A@0
10. (arrow(A) A1 A@0 x y1) = x1 ∈ (ob(A) A@0)
⊢ (arrow(B) A1 A@0 x (m A1 y1)) = (m A@0 x1) ∈ (ob(B) A@0)

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  A  :  Presheaf(C)
3.  B  :  Presheaf(C)
4.  m  :  A  {}\mrightarrow{}  B
5.  A@0  :  cat-ob(op-cat(C))
6.  x1  :  ob(A)  A@0
7.  A1  :  cat-ob(op-cat(C))
8.  y1  :  ob(A)  A1
9.  x  :  \{f:cat-arrow(op-cat(C))  A1  A@0|  (arrow(A)  A1  A@0  f  y1)  =  x1\} 
\mvdash{}  x  \mmember{}  \{f:cat-arrow(op-cat(C))  A1  A@0|  (arrow(B)  A1  A@0  f  (m  A1  y1))  =  (m  A@0  x1)\} 


By

---

Latex:
(D  -1  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  MemTypeCD\mcdot{}  THEN  Auto)

---

Home Index