---

Step * 1 1 1 of Lemma existssetmem_functionality


1. A : coSet{i:l}
2. P : {a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ
3. B : coSet{i:l}
4. set-predicate{i:l}(A;a.P[a])
5. seteq(A;B)
6. set-predicate{i:l}(B;a.P[a])
7. ∀a:coSet{i:l}. ((a ∈ B) ⇒ (a ∈ A))
⊢ ∃a:coSet{i:l}. ((a ∈ A) ∧ P[a]) ⇐⇒ ∃a:coSet{i:l}. ((a ∈ B) ∧ P[a])
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN ParallelLast) }

1
1. A : coSet{i:l}
2. P : {a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ
3. B : coSet{i:l}
4. set-predicate{i:l}(A;a.P[a])
5. seteq(A;B)
6. set-predicate{i:l}(B;a.P[a])
7. ∀a:coSet{i:l}. ((a ∈ B) ⇒ (a ∈ A))
8. a : coSet{i:l}
9. (a ∈ A) ∧ P[a]
⊢ (a ∈ B) ∧ P[a]

2
1. A : coSet{i:l}
2. P : {a:coSet{i:l}| (a ∈ A)}  ⟶ ℙ
3. B : coSet{i:l}
4. set-predicate{i:l}(A;a.P[a])
5. seteq(A;B)
6. set-predicate{i:l}(B;a.P[a])
7. ∀a:coSet{i:l}. ((a ∈ B) ⇒ (a ∈ A))
8. a : coSet{i:l}
9. (a ∈ B) ∧ P[a]
⊢ (a ∈ A) ∧ P[a]

---

Latex:

---

Latex:

1.  A  :  coSet\{i:l\}
2.  P  :  \{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  \mBbbP{}
3.  B  :  coSet\{i:l\}
4.  set-predicate\{i:l\}(A;a.P[a])
5.  seteq(A;B)
6.  set-predicate\{i:l\}(B;a.P[a])
7.  \mforall{}a:coSet\{i:l\}.  ((a  \mmember{}  B)  {}\mRightarrow{}  (a  \mmember{}  A))
\mvdash{}  \mexists{}a:coSet\{i:l\}.  ((a  \mmember{}  A)  \mwedge{}  P[a])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:coSet\{i:l\}.  ((a  \mmember{}  B)  \mwedge{}  P[a])


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  ParallelLast)

---

Home Index