---

Step * of Lemma setmem-intersectionset

∀s,x:coSet{i:l}.  ((∃a:coSet{i:l}. (a ∈ s)) ⇒ ((x ∈ ⋂(s)) ⇐⇒ ∀z:coSet{i:l}. ((z ∈ s) ⇒ (x ∈ z))))
BY
{ ((UnivCD THENA Auto) THEN Unfold `intersectionset` 0 THEN (RWO "setmem-sub-coset" 0 THENA Auto)) }

1
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))

---

Latex:

---

Latex:
\mforall{}s,x:coSet\{i:l\}.    ((\mexists{}a:coSet\{i:l\}.  (a  \mmember{}  s))  {}\mRightarrow{}  ((x  \mmember{}  \mcap{}(s))  \mLeftarrow{}{}\mRightarrow{}  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  s)  {}\mRightarrow{}  (x  \mmember{}  z))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `intersectionset`  0  THEN  (RWO  "setmem-sub-coset"  0  THENA  Auto))

---

Home Index