---

Step * of Lemma poset-cat-ob-cases

∀I:Cname List. ∀c1,c2:cat-ob(poset-cat(I)).  ((c1 = c2 ∈ cat-ob(poset-cat(I))) ∨ (∃y:nameset(I). c1 y ≠ c2 y))
BY
{ ((UnivCD THENA Auto)
   THEN All
   (RepUR ``cat-ob poset-cat``)⋅
   THEN (Assert I ∈ nameset(I) List BY
               (Unfold `nameset` 0 THEN Auto))
   THEN (Decide ⌜(∃y∈I. c1 y ≠ c2 y)⌝⋅ THENA Auto)) }

1
1. I : Cname List
2. c1 : name-morph(I;[])
3. c2 : name-morph(I;[])
4. I ∈ nameset(I) List
5. (∃y∈I. c1 y ≠ c2 y)
⊢ (c1 = c2 ∈ name-morph(I;[])) ∨ (∃y:nameset(I). c1 y ≠ c2 y)

2
1. I : Cname List
2. c1 : name-morph(I;[])
3. c2 : name-morph(I;[])
4. I ∈ nameset(I) List
5. ¬(∃y∈I. c1 y ≠ c2 y)
⊢ (c1 = c2 ∈ name-morph(I;[])) ∨ (∃y:nameset(I). c1 y ≠ c2 y)

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  \mforall{}c1,c2:cat-ob(poset-cat(I)).    ((c1  =  c2)  \mvee{}  (\mexists{}y:nameset(I).  c1  y  \mneq{}  c2  y))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  All
  (RepUR  ``cat-ob  poset-cat``)\mcdot{}
  THEN  (Assert  I  \mmember{}  nameset(I)  List  BY
                          (Unfold  `nameset`  0  THEN  Auto))
  THEN  (Decide  \mkleeneopen{}(\mexists{}y\mmember{}I.  c1  y  \mneq{}  c2  y)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index