---

Step * 1 of Lemma decidable__equal-poset-cat-ob


1. I : Cname List@i
2. c1 : cat-ob(poset-cat(I))@i
3. c2 : cat-ob(poset-cat(I))@i
4. ∃y:nameset(I). c1 y ≠ c2 y
⊢ ¬(c1 = c2 ∈ cat-ob(poset-cat(I)))
BY
{ ((D 0 THENA Auto) THEN ExRepD THEN D -2) }

1
1. I : Cname List@i
2. c1 : cat-ob(poset-cat(I))@i
3. c2 : cat-ob(poset-cat(I))@i
4. y : nameset(I)
5. c1 = c2 ∈ cat-ob(poset-cat(I))@i
⊢ (c1 y) = (c2 y) ∈ ℤ

---

Latex:

---

Latex:

1.  I  :  Cname  List@i
2.  c1  :  cat-ob(poset-cat(I))@i
3.  c2  :  cat-ob(poset-cat(I))@i
4.  \mexists{}y:nameset(I).  c1  y  \mneq{}  c2  y
\mvdash{}  \mneg{}(c1  =  c2)


By

---

Latex:
((D  0  THENA  Auto)  THEN  ExRepD  THEN  D  -2)

---

Home Index