---

Step * 1 1 1 1 of Lemma cosetTC_functionality_subset


1. a : coSet{i:l}
2. b : coSet{i:l}
3. ∀x:coSet{i:l}. ((x ∈ a) ⇒ (x ∈ b))
4. n : ℕ
5. t1 : coPath(T.T;a;n)
6. 0 < n
⊢ ∃p:coPath(T.T;b;n). seteq(coPath-at(n;a;t1);coPath-at(n;b;p))
BY
{ (MoveToConcl (-2) THEN RepeatFor 3 (MoveToConcl (-3)) THEN RepUR ``coSet seteq setmem`` 0 THEN NatInd 1 THEN Auto) }

1
1. n : ℤ
2. [%1] : 0 < n
3. 0 < n - 1
⇒ (∀a,b:coW(Type;x.x).
      ((∀x:coW(Type;x.x). (coWmem(T.T;x;a) ⇒ coWmem(T.T;x;b)))
      ⇒ (∀t1:coPath(T.T;a;n - 1). ∃p:coPath(T.T;b;n - 1). coW-equiv(T.T;coPath-at(n - 1;a;t1);coPath-at(n - 1;b;p)))))
4. 0 < n
5. a : coW(Type;x.x)
6. b : coW(Type;x.x)
7. ∀x:coW(Type;x.x). (coWmem(T.T;x;a) ⇒ coWmem(T.T;x;b))
8. t1 : coPath(T.T;a;n)
⊢ ∃p:coPath(T.T;b;n). coW-equiv(T.T;coPath-at(n;a;t1);coPath-at(n;b;p))

---

Latex:

---

Latex:

1.  a  :  coSet\{i:l\}
2.  b  :  coSet\{i:l\}
3.  \mforall{}x:coSet\{i:l\}.  ((x  \mmember{}  a)  {}\mRightarrow{}  (x  \mmember{}  b))
4.  n  :  \mBbbN{}
5.  t1  :  coPath(T.T;a;n)
6.  0  <  n
\mvdash{}  \mexists{}p:coPath(T.T;b;n).  seteq(coPath-at(n;a;t1);coPath-at(n;b;p))


By

---

Latex:
(MoveToConcl  (-2)
  THEN  RepeatFor  3  (MoveToConcl  (-3))
  THEN  RepUR  ``coSet  seteq  setmem``  0
  THEN  NatInd  1
  THEN  Auto)

---

Home Index