---

Step * of Lemma implies-setmem-piset

No Annotations
∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}. ∀x:coSet{i:l}.
  ((∀a1,a2:coSet{i:l}.  ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2])))
  ⇒ ((x ⊆ Σa:A.B[a])
     ∧ (∀a:coSet{i:l}. ((a ∈ A) ⇒ (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ ((a,b) ∈ x)))))
     ∧ (∀a,b1,b2:coSet{i:l}.  ((a ∈ A) ⇒ (b1 ∈ B[a]) ⇒ (b2 ∈ B[a]) ⇒ ((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2))))
  ⇒ (x ∈ piset(A;a.B[a])))
BY
{ (Intro
   THEN (Assert ∀t:set-dom(A). (set-item(A;t) ∈ {a:coSet{i:l}| (a ∈ A)} ) BY
               ((Auto THEN MemTypeCD THEN Auto) THEN RWO "setmem-iff" 0 THEN Auto))
   THEN Auto
   THEN (RWO "setmem-piset-1" 0 THENA Auto)) }

1
1. A : coSet{i:l}
2. ∀t:set-dom(A). (set-item(A;t) ∈ {a:coSet{i:l}| (a ∈ A)} )
3. B : {a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}
4. x : coSet{i:l}
5. ∀a1,a2:coSet{i:l}.  ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2]))
6. (x ⊆ Σa:A.B[a])
7. ∀a:coSet{i:l}. ((a ∈ A) ⇒ (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ ((a,b) ∈ x))))
8. ∀a,b1,b2:coSet{i:l}.  ((a ∈ A) ⇒ (b1 ∈ B[a]) ⇒ (b2 ∈ B[a]) ⇒ ((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2))
⊢ ∃f:t:set-dom(A) ⟶ set-dom(B[set-item(A;t)])
   ∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ ∃t:set-dom(A). seteq(z;(set-item(A;t),set-item(B[set-item(A;t)];f t))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}A:coSet\{i:l\}.  \mforall{}B:\{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  coSet\{i:l\}.  \mforall{}x: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{}  ((x  \msubseteq{}  \mSigma{}a:A.B[a])
          \mwedge{}  (\mforall{}a:coSet\{i:l\}.  ((a  \mmember{}  A)  {}\mRightarrow{}  (\mexists{}b:coSet\{i:l\}.  ((b  \mmember{}  B[a])  \mwedge{}  ((a,b)  \mmember{}  x)))))
          \mwedge{}  (\mforall{}a,b1,b2:coSet\{i:l\}.
                    ((a  \mmember{}  A)  {}\mRightarrow{}  (b1  \mmember{}  B[a])  {}\mRightarrow{}  (b2  \mmember{}  B[a])  {}\mRightarrow{}  ((a,b1)  \mmember{}  x)  {}\mRightarrow{}  ((a,b2)  \mmember{}  x)  {}\mRightarrow{}  seteq(b1;b2))))
    {}\mRightarrow{}  (x  \mmember{}  piset(A;a.B[a])))


By

---

Latex:
(Intro
  THEN  (Assert  \mforall{}t:set-dom(A).  (set-item(A;t)  \mmember{}  \{a:coSet\{i:l\}|  (a  \mmember{}  A)\}  )  BY
                          ((Auto  THEN  MemTypeCD  THEN  Auto)  THEN  RWO  "setmem-iff"  0  THEN  Auto))
  THEN  Auto
  THEN  (RWO  "setmem-piset-1"  0  THENA  Auto))

---

Home Index