---

Step * of Lemma setmem-sigmaset

∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}.
  ((∀a1,a2:coSet{i:l}.  ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2])))
  ⇒ (∀x:coSet{i:l}. ((x ∈ Σa:A.B[a]) ⇐⇒ ∃a:coSet{i:l}. ((a ∈ A) ∧ (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ seteq(x;(a,b))))))))
BY
{ (Auto THEN ExRepD) }

1
1. A : coSet{i:l}
2. B : {a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}
3. ∀a1,a2:coSet{i:l}.  ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2]))
4. x : coSet{i:l}
5. (x ∈ Σa:A.B[a])
⊢ ∃a:coSet{i:l}. ((a ∈ A) ∧ (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ seteq(x;(a,b)))))

2
1. A : coSet{i:l}
2. B : {a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}
3. ∀a1,a2:coSet{i:l}.  ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2]))
4. x : coSet{i:l}
5. a : coSet{i:l}
6. (a ∈ A)
7. b : coSet{i:l}
8. (b ∈ B[a])
9. seteq(x;(a,b))
⊢ (x ∈ Σa:A.B[a])

---

Latex:

---

Latex:
\mforall{}A:coSet\{i:l\}.  \mforall{}B:\{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  coSet\{i:l\}.
    ((\mforall{}a1,a2:coSet\{i:l\}.    ((a1  \mmember{}  A)  {}\mRightarrow{}  (a2  \mmember{}  A)  {}\mRightarrow{}  seteq(a1;a2)  {}\mRightarrow{}  seteq(B[a1];B[a2])))
    {}\mRightarrow{}  (\mforall{}x:coSet\{i:l\}
                ((x  \mmember{}  \mSigma{}a:A.B[a])
                \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:coSet\{i:l\}.  ((a  \mmember{}  A)  \mwedge{}  (\mexists{}b:coSet\{i:l\}.  ((b  \mmember{}  B[a])  \mwedge{}  seteq(x;(a,b))))))))


By

---

Latex:
(Auto  THEN  ExRepD)

---

Home Index