---

Step * 1 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)
5. c1 = c2 ∈ cat-ob(poset-cat(I))@i
⊢ (c1 y) = (c2 y) ∈ ℤ
BY
{ (All (RepUR ``poset-cat cat-ob name-morph``)⋅ THEN (EqTypeHD (-1) THENA Auto)) }

1
1. I : Cname List@i
2. c1 : {f:nameset(I) ⟶ extd-nameset([])| 
         ∀i,j:nameset(I).
           ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset([])) ⇒ (i = j ∈ nameset(I)))} @i
3. c2 : {f:nameset(I) ⟶ extd-nameset([])| 
         ∀i,j:nameset(I).
           ((↑isname(f i)) ⇒ (↑isname(f j)) ⇒ ((f i) = (f j) ∈ extd-nameset([])) ⇒ (i = j ∈ nameset(I)))} @i
4. y : nameset(I)
5. c1 = c2 ∈ (nameset(I) ⟶ extd-nameset([]))
6. ∀i,j:nameset(I).
     ((↑isname(c1 i)) ⇒ (↑isname(c1 j)) ⇒ ((c1 i) = (c1 j) ∈ extd-nameset([])) ⇒ (i = j ∈ nameset(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.  y  :  nameset(I)
5.  c1  =  c2@i
\mvdash{}  (c1  y)  =  (c2  y)


By

---

Latex:
(All  (RepUR  ``poset-cat  cat-ob  name-morph``)\mcdot{}  THEN  (EqTypeHD  (-1)  THENA  Auto))

---

Home Index