---

Step * 1 1 2 1 1 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)
4. T : Type
5. X1 : T ⟶ coSet{i:l}
6. seteq(<T, X1>;f"(a))
7. ∀z:coSet{i:l}. ((z ∈ <T, X1>) ⇒ (z ∈ Set{i:l}))
8. x : T
⊢ ∃t:set-dom(<T, X1>). seteq(X1 x;set-item(<T, X1>;t))
BY
{ (RepUR ``set-dom set-item`` 0 THEN D 0 With ⌜x⌝  THEN Auto) }

1
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. T : Type
5. X1 : T ⟶ coSet{i:l}
6. seteq(<T, X1>;f"(a))
7. ∀z:coSet{i:l}. ((z ∈ <T, X1>) ⇒ (z ∈ Set{i:l}))
8. x : T
⊢ seteq(X1 x;X1 x)

---

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)
4.  T  :  Type
5.  X1  :  T  {}\mrightarrow{}  coSet\{i:l\}
6.  seteq(<T,  X1>f"(a))
7.  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  <T,  X1>)  {}\mRightarrow{}  (z  \mmember{}  Set\{i:l\}))
8.  x  :  T
\mvdash{}  \mexists{}t:set-dom(<T,  X1>).  seteq(X1  x;set-item(<T,  X1>t))


By

---

Latex:
(RepUR  ``set-dom  set-item``  0  THEN  D  0  With  \mkleeneopen{}x\mkleeneclose{}    THEN  Auto)

---

Home Index