---

Step * 1 1 of Lemma coSet-seteq-Set

.....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}
BY
{ (RenameVar `X' (-2) THEN Assert ⌜∀z:coSet{i:l}. ((z ∈ X) ⇒ (z ∈ Set{i:l}))⌝⋅) }

1
.....assertion..... 
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. X : coSet{i:l}
5. seteq(X;f"(a))
⊢ ∀z:coSet{i:l}. ((z ∈ X) ⇒ (z ∈ Set{i:l}))

2
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. X : coSet{i:l}
5. seteq(X;f"(a))
6. ∀z:coSet{i:l}. ((z ∈ X) ⇒ (z ∈ Set{i:l}))
⊢ X ∈ Set{i:l}

---

Latex:

---

Latex:
.....eq  aux..... 
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)
4.  z@0  :  coSet\{i:l\}
5.  seteq(z@0;f"(a))
\mvdash{}  z@0  \mmember{}  Set\{i:l\}


By

---

Latex:
(RenameVar  `X'  (-2)  THEN  Assert  \mkleeneopen{}\mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  X)  {}\mRightarrow{}  (z  \mmember{}  Set\{i:l\}))\mkleeneclose{}\mcdot{})

---

Home Index