Step * 1 1 2 of Lemma coSet-seteq-Set


1. Type
2. a ⟶ W(Type;a.a)
3. ∀b:a. ∀[z:coSet{i:l}]. z ∈ Set{i:l} supposing seteq(z;f b)
4. coSet{i:l}
5. seteq(X;f"(a))
6. ∀z:coSet{i:l}. ((z ∈ X)  (z ∈ Set{i:l}))
⊢ X ∈ Set{i:l}
BY
((coSetD THEN 4)
   THEN (Fold `Wsup` THEN Fold `mk-set` 0)
   THEN MemCD
   THEN (Declaration ORELSE FunExt)
   THEN Try (Declaration)) }

1
1. Type
2. a ⟶ W(Type;a.a)
3. ∀b:a. ∀[z:coSet{i:l}]. z ∈ Set{i:l} supposing seteq(z;f b)
4. 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. T
⊢ X1 x ∈ 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)
4.  X  :  coSet\{i:l\}
5.  seteq(X;f"(a))
6.  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  X)  {}\mRightarrow{}  (z  \mmember{}  Set\{i:l\}))
\mvdash{}  X  \mmember{}  Set\{i:l\}


By


Latex:
((coSetD  4  THEN  D  4)
  THEN  (Fold  `Wsup`  0  THEN  Fold  `mk-set`  0)
  THEN  MemCD
  THEN  (Declaration  ORELSE  FunExt)
  THEN  Try  (Declaration))




Home Index