---

Step * of Lemma poset-cat-arrow-unique

∀[I:Cname List]. ∀[x,y:cat-ob(poset-cat(I))]. ∀[a,b:cat-arrow(poset-cat(I)) x y].
  (a = b ∈ (cat-arrow(poset-cat(I)) x y))
BY
{ (RepUR ``cat-ob cat-arrow poset-cat all`` 0
   THEN Auto
   THEN FunExt
   THEN Auto
   THEN GenConclAtAddr [2]
   THEN GenConclAtAddr [3]
   THEN ∀h:hyp. (UnfoldTop `assert` h THEN (SplitOnHypITE h  THENA Auto) THEN Try (Trivial)) ) }

1
.....truecase..... 
1. I : Cname List
2. x : name-morph(I;[])
3. y : name-morph(I;[])
4. a : x@0:nameset(I) ⟶ (↑x x@0 ≤z y x@0)
5. b : x@0:nameset(I) ⟶ (↑x x@0 ≤z y x@0)
6. x@0 : nameset(I)
7. v : True@i
8. (a x@0) = v ∈ (↑x x@0 ≤z y x@0)@i
9. v1 : True@i
10. (b x@0) = v1 ∈ (↑x x@0 ≤z y x@0)@i
11. (x x@0) ≤ (y x@0)
12. (x x@0) ≤ (y x@0)
⊢ v = v1 ∈ (↑x x@0 ≤z y x@0)

---

Latex:

---

Latex:
\mforall{}[I:Cname  List].  \mforall{}[x,y:cat-ob(poset-cat(I))].  \mforall{}[a,b:cat-arrow(poset-cat(I))  x  y].    (a  =  b)


By

---

Latex:
(RepUR  ``cat-ob  cat-arrow  poset-cat  all``  0
  THEN  Auto
  THEN  FunExt
  THEN  Auto
  THEN  GenConclAtAddr  [2]
  THEN  GenConclAtAddr  [3]
  THEN  \mforall{}h:hyp.  (UnfoldTop  `assert`  h  THEN  (SplitOnHypITE  h    THENA  Auto)  THEN  Try  (Trivial))  )

---

Home Index