---

Step * 1 of Lemma setmem-intersectionset


1. s : coSet{i:l}
2. x : coSet{i:l}
3. ∃a:coSet{i:l}. (a ∈ s)
⊢ (x ∈ ⋃(s)) ∧ ∀z∈s.(x ∈ z) ⇐⇒ ∀z:coSet{i:l}. ((z ∈ s) ⇒ (x ∈ z))
BY
{ ((RWO "setmem-unionset" 0 THENA Auto) THEN RWO "allsetmem-iff" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  coSet\{i:l\}
2.  x  :  coSet\{i:l\}
3.  \mexists{}a:coSet\{i:l\}.  (a  \mmember{}  s)
\mvdash{}  (x  \mmember{}  \mcup{}(s))  \mwedge{}  \mforall{}z\mmember{}s.(x  \mmember{}  z)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  s)  {}\mRightarrow{}  (x  \mmember{}  z))


By

---

Latex:
((RWO  "setmem-unionset"  0  THENA  Auto)  THEN  RWO  "allsetmem-iff"  0  THEN  Auto)

---

Home Index