---

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


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) ∈ ℤ
BY
{ (EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Cname  List@i
2.  c1  :  \{f:nameset(I)  {}\mrightarrow{}  extd-nameset([])| 
                  \mforall{}i,j:nameset(I).    ((\muparrow{}isname(f  i))  {}\mRightarrow{}  (\muparrow{}isname(f  j))  {}\mRightarrow{}  ((f  i)  =  (f  j))  {}\mRightarrow{}  (i  =  j))\}  @i
3.  c2  :  \{f:nameset(I)  {}\mrightarrow{}  extd-nameset([])| 
                  \mforall{}i,j:nameset(I).    ((\muparrow{}isname(f  i))  {}\mRightarrow{}  (\muparrow{}isname(f  j))  {}\mRightarrow{}  ((f  i)  =  (f  j))  {}\mRightarrow{}  (i  =  j))\}  @i
4.  y  :  nameset(I)
5.  c1  =  c2
6.  \mforall{}i,j:nameset(I).    ((\muparrow{}isname(c1  i))  {}\mRightarrow{}  (\muparrow{}isname(c1  j))  {}\mRightarrow{}  ((c1  i)  =  (c1  j))  {}\mRightarrow{}  (i  =  j))
\mvdash{}  (c1  y)  =  (c2  y)


By

---

Latex:
(EqCD  THEN  Auto)

---

Home Index