---

Step * 1 of Lemma poset-cat-arrow-equals

.....wf..... 
1. I : Cname List
2. x : cat-ob(poset-cat(I))
3. y : cat-ob(poset-cat(I))
4. a : cat-arrow(poset-cat(I)) x y
⊢ λx.Ax ∈ cat-arrow(poset-cat(I)) x y
BY
{ (All (RepUR ``cat-arrow cat-ob poset-cat``) THEN Unfold `all` 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  Cname  List
2.  x  :  cat-ob(poset-cat(I))
3.  y  :  cat-ob(poset-cat(I))
4.  a  :  cat-arrow(poset-cat(I))  x  y
\mvdash{}  \mlambda{}x.Ax  \mmember{}  cat-arrow(poset-cat(I))  x  y


By

---

Latex:
(All  (RepUR  ``cat-arrow  cat-ob  poset-cat``)  THEN  Unfold  `all`  0  THEN  Auto)

---

Home Index