---

Step * 1 1 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. X : coSet{i:l}
5. ∀z:coSet{i:l}. ((z ∈ X) ⇐⇒ (z ∈ f"(a)))
6. z : coSet{i:l}@i'
7. (z ∈ X) ⇐ (z ∈ f"(a))
8. (z ∈ X)
9. ∃t:set-dom(f"(a)). seteq(z;set-item(f"(a);t))
⊢ z ∈ Set{i:l}
BY
{ (RepUR ``set-dom set-item mk-set Wsup`` -1 THEN D -1 THEN (D 3 With ⌜t⌝  THENA Auto) THEN BHyp -1 THEN Auto) }

---

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.  X  :  coSet\{i:l\}
5.  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  X)  \mLeftarrow{}{}\mRightarrow{}  (z  \mmember{}  f"(a)))
6.  z  :  coSet\{i:l\}@i'
7.  (z  \mmember{}  X)  \mLeftarrow{}{}  (z  \mmember{}  f"(a))
8.  (z  \mmember{}  X)
9.  \mexists{}t:set-dom(f"(a)).  seteq(z;set-item(f"(a);t))
\mvdash{}  z  \mmember{}  Set\{i:l\}


By

---

Latex:
(RepUR  ``set-dom  set-item  mk-set  Wsup``  -1
  THEN  D  -1
  THEN  (D  3  With  \mkleeneopen{}t\mkleeneclose{}    THENA  Auto)
  THEN  BHyp  -1
  THEN  Auto)

---

Home Index