---

Step * of Lemma existssetmem-iff

∀A:coSet{i:l}
  ∀[P:{a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ]. (set-predicate{i:l}(A;a.P[a]) ⇒ (∃a∈A.P[a] ⇐⇒ ∃a:coSet{i:l}. ((a ∈ A) ∧ P[a])))
BY
{ ((Intros THEN Try ((UniverseIsType THEN Fold `member` 0 THEN BLemma `set-predicate_wf` THEN Auto)))
   THEN (Auto THEN coSetD 1 THEN D 1)
   THEN All (Fold `mk-coset`)) }

1
1. T : Type
2. A1 : T ⟶ coSet{i:l}
3. [P] : {a:coSet{i:l}| (a ∈ mk-coset(T;A1))}  ⟶ ℙ
4. set-predicate{i:l}(mk-coset(T;A1);a.P[a])
5. ∃a∈mk-coset(T;A1).P[a]
⊢ ∃a:coSet{i:l}. ((a ∈ mk-coset(T;A1)) ∧ P[a])

2
1. T : Type
2. A1 : T ⟶ coSet{i:l}
3. [P] : {a:coSet{i:l}| (a ∈ mk-coset(T;A1))}  ⟶ ℙ
4. set-predicate{i:l}(mk-coset(T;A1);a.P[a])
5. ∃a:coSet{i:l}. ((a ∈ mk-coset(T;A1)) ∧ P[a])
⊢ ∃a∈mk-coset(T;A1).P[a]

---

Latex:

---

Latex:
\mforall{}A:coSet\{i:l\}
    \mforall{}[P:\{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  \mBbbP{}]
        (set-predicate\{i:l\}(A;a.P[a])  {}\mRightarrow{}  (\mexists{}a\mmember{}A.P[a]  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:coSet\{i:l\}.  ((a  \mmember{}  A)  \mwedge{}  P[a])))


By

---

Latex:
((Intros  THEN  Try  ((UniverseIsType  THEN  Fold  `member`  0  THEN  BLemma  `set-predicate\_wf`  THEN  Auto)))
  THEN  (Auto  THEN  coSetD  1  THEN  D  1)
  THEN  All  (Fold  `mk-coset`))

---

Home Index