---

Step * 2 1 of Lemma setmem-piset-implies


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. f : t:set-dom(A) ⟶ set-dom(B[set-item(A;t)])
7. ∀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))))
8. (x ⊆ Σa:A.B[a])
9. a : coSet{i:l}
10. t : set-dom(A)
11. seteq(a;set-item(A;t))
⊢ ∃b:coSet{i:l}. ((b ∈ B[a]) ∧ (∃t:set-dom(A). seteq((a,b);(set-item(A;t),set-item(B[set-item(A;t)];f t)))))
BY
{ ((Assert (set-item(A;t) ∈ A) BY
          (RWO  "setmem-iff" 0 THEN Auto))
   THEN (Assert (a ∈ A) BY
               (RWO "-2" 0 THEN Auto))
   THEN (Assert seteq(B[a];B[set-item(A;t)]) BY
               (BackThruSomeHyp THEN 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. f : t:set-dom(A) ⟶ set-dom(B[set-item(A;t)])
7. ∀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))))
8. (x ⊆ Σa:A.B[a])
9. a : coSet{i:l}
10. t : set-dom(A)
11. seteq(a;set-item(A;t))
12. (set-item(A;t) ∈ A)
13. (a ∈ A)
14. seteq(B[a];B[set-item(A;t)])
⊢ ∃b:coSet{i:l}. ((b ∈ B[a]) ∧ (∃t:set-dom(A). seteq((a,b);(set-item(A;t),set-item(B[set-item(A;t)];f t)))))

---

Latex:

---

Latex:

1.  A  :  coSet\{i:l\}
2.  \mforall{}t:set-dom(A).  (set-item(A;t)  \mmember{}  \{a:coSet\{i:l\}|  (a  \mmember{}  A)\}  )
3.  B  :  \{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  coSet\{i:l\}
4.  x  :  coSet\{i:l\}
5.  \mforall{}a1,a2:coSet\{i:l\}.    ((a1  \mmember{}  A)  {}\mRightarrow{}  (a2  \mmember{}  A)  {}\mRightarrow{}  seteq(a1;a2)  {}\mRightarrow{}  seteq(B[a1];B[a2]))
6.  f  :  t:set-dom(A)  {}\mrightarrow{}  set-dom(B[set-item(A;t)])
7.  \mforall{}z:coSet\{i:l\}
          ((z  \mmember{}  x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}t:set-dom(A).  seteq(z;(set-item(A;t),set-item(B[set-item(A;t)];f  t))))
8.  (x  \msubseteq{}  \mSigma{}a:A.B[a])
9.  a  :  coSet\{i:l\}
10.  t  :  set-dom(A)
11.  seteq(a;set-item(A;t))
\mvdash{}  \mexists{}b:coSet\{i:l\}
      ((b  \mmember{}  B[a])  \mwedge{}  (\mexists{}t:set-dom(A).  seteq((a,b);(set-item(A;t),set-item(B[set-item(A;t)];f  t)))))


By

---

Latex:
((Assert  (set-item(A;t)  \mmember{}  A)  BY
                (RWO    "setmem-iff"  0  THEN  Auto))
  THEN  (Assert  (a  \mmember{}  A)  BY
                          (RWO  "-2"  0  THEN  Auto))
  THEN  (Assert  seteq(B[a];B[set-item(A;t)])  BY
                          (BackThruSomeHyp  THEN  Auto)))

---

Home Index