---

Step * 1 of Lemma allsetmem-iff


1. A : coSet{i:l}
2. [P] : {a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ
3. set-predicate{i:l}(A;a.P[a])
⊢ ∀a∈A.P[a] ⇐⇒ ∀a:coSet{i:l}. ((a ∈ A) ⇒ P[a])
BY
{ ((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]
6. a : coSet{i:l}
7. (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:

1.  A  :  coSet\{i:l\}
2.  [P]  :  \{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  \mBbbP{}
3.  set-predicate\{i:l\}(A;a.P[a])
\mvdash{}  \mforall{}a\mmember{}A.P[a]  \mLeftarrow{}{}\mRightarrow{}  \mforall{}a:coSet\{i:l\}.  ((a  \mmember{}  A)  {}\mRightarrow{}  P[a])


By

---

Latex:
((Auto  THEN  coSetD  1  THEN  D  1)  THEN  All  (Fold  `mk-coset`))

---

Home Index