---

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


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 : ∀x:nameset(I). (↑c1 x ≤z c2 x)
7. (c1 y) ≤ (c2 y)
⊢ ((c1 y) = 0 ∈ ℕ2) ∧ ((c2 y) = 1 ∈ ℕ2)
BY
{ ((MoveToConcl (-1) THEN MoveToConcl (-2))
   THEN (GenConcl ⌜(c1 y) = a ∈ ℕ2⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(c2 y) = b ∈ ℕ2⌝⋅ 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. f : ∀x:nameset(I). (↑c1 x ≤z c2 x)
6. a : ℕ2
7. (c1 y) = a ∈ ℕ2
8. b : ℕ2
9. (c2 y) = b ∈ ℕ2
⊢ a ≠ b ⇒ (a ≤ b) ⇒ ((a = 0 ∈ ℕ2) ∧ (b = 1 ∈ ℕ2))

---

Latex:

---

Latex:

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  \mneq{}  c2  y
6.  f  :  \mforall{}x:nameset(I).  (\muparrow{}c1  x  \mleq{}z  c2  x)
7.  (c1  y)  \mleq{}  (c2  y)
\mvdash{}  ((c1  y)  =  0)  \mwedge{}  ((c2  y)  =  1)


By

---

Latex:
((MoveToConcl  (-1)  THEN  MoveToConcl  (-2))
  THEN  (GenConcl  \mkleeneopen{}(c1  y)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(c2  y)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index