---

Step * 1 of Lemma coSet-seteq-Set


1. a : Type
2. f : a ⟶ W(Type;a.a)
3. ∀b:a. ∀[z:coSet{i:l}]. z ∈ Set{i:l} supposing seteq(z;f b)
⊢ Ax ∈ ∀[z@0:coSet{i:l}]. z@0 ∈ Set{i:l} supposing seteq(z@0;Wsup(a;f))
BY
{ (Fold `mk-set` 0
   THEN (Unfold `uall` 0 THEN (MemTypeCD THENW Auto))
   THEN Unfold `uimplies` 0
   THEN (MemTypeCD THENW Auto)
   THEN MemCD) }

1
.....eq aux..... 
1. a : Type
2. f : a ⟶ W(Type;a.a)
3. ∀b:a. ∀[z:coSet{i:l}]. z ∈ Set{i:l} supposing seteq(z;f b)
4. z@0 : coSet{i:l}
5. seteq(z@0;f"(a))
⊢ z@0 ∈ Set{i:l}

---

Latex:

---

Latex:

1.  a  :  Type
2.  f  :  a  {}\mrightarrow{}  W(Type;a.a)
3.  \mforall{}b:a.  \mforall{}[z:coSet\{i:l\}].  z  \mmember{}  Set\{i:l\}  supposing  seteq(z;f  b)
\mvdash{}  Ax  \mmember{}  \mforall{}[z@0:coSet\{i:l\}].  z@0  \mmember{}  Set\{i:l\}  supposing  seteq(z@0;Wsup(a;f))


By

---

Latex:
(Fold  `mk-set`  0
  THEN  (Unfold  `uall`  0  THEN  (MemTypeCD  THENW  Auto))
  THEN  Unfold  `uimplies`  0
  THEN  (MemTypeCD  THENW  Auto)
  THEN  MemCD)

---

Home Index