Step
*
of Lemma
setmem-unionset
∀s,x:coSet{i:l}.  ((x ∈ ⋃(s)) 
⇐⇒ ∃a:coSet{i:l}. ((a ∈ s) ∧ (x ∈ a)))
BY
{ (Intros
   THEN (Assert ∀s:coSet{i:l}. set-function{i:l}(s; x1.x1) BY
               RepeatFor 2 ((D 0 THEN Auto)))
   THEN Unfold `unionset` 0
   THEN RWO "setmem-setunionfun" 0
   THEN Auto) }
Latex:
Latex:
\mforall{}s,x:coSet\{i:l\}.    ((x  \mmember{}  \mcup{}(s))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:coSet\{i:l\}.  ((a  \mmember{}  s)  \mwedge{}  (x  \mmember{}  a)))
By
Latex:
(Intros
  THEN  (Assert  \mforall{}s:coSet\{i:l\}.  set-function\{i:l\}(s;  x1.x1)  BY
                          RepeatFor  2  ((D  0  THEN  Auto)))
  THEN  Unfold  `unionset`  0
  THEN  RWO  "setmem-setunionfun"  0
  THEN  Auto)
Home
Index