---

Step * of Lemma poset-cat-arrow-not-equal

∀I:Cname List. ∀y:nameset(I). ∀c1,c2:cat-ob(poset-cat(I)).
  (c1 y ≠ c2 y ⇒ (∀f:cat-arrow(poset-cat(I)) c1 c2. (((c1 y) = 0 ∈ ℕ2) ∧ ((c2 y) = 1 ∈ ℕ2))))
BY
{ (UnivCD THENA Auto) }

1
1. I : Cname List
2. y : nameset(I)
3. c1 : cat-ob(poset-cat(I))
4. c2 : cat-ob(poset-cat(I))
5. c1 y ≠ c2 y
6. f : cat-arrow(poset-cat(I)) c1 c2
⊢ ((c1 y) = 0 ∈ ℕ2) ∧ ((c2 y) = 1 ∈ ℕ2)

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  \mforall{}y:nameset(I).  \mforall{}c1,c2:cat-ob(poset-cat(I)).
    (c1  y  \mneq{}  c2  y  {}\mRightarrow{}  (\mforall{}f:cat-arrow(poset-cat(I))  c1  c2.  (((c1  y)  =  0)  \mwedge{}  ((c2  y)  =  1))))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index