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 ((D 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