---

Step * of Lemma setmem-piset-1

∀A:coSet{i:l}. ∀B:{a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}. ∀x:coSet{i:l}.
  ((x ∈ piset(A;a.B[a]))
  ⇐⇒ ∃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)))))
BY
{ (Auto THEN ExRepD) }

1
1. A : coSet{i:l}
2. B : {a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}
3. x : coSet{i:l}
4. (x ∈ piset(A;a.B[a]))
⊢ ∃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))))

2
1. A : coSet{i:l}
2. B : {a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}
3. x : coSet{i:l}
4. f : t:set-dom(A) ⟶ set-dom(B[set-item(A;t)])
5. ∀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))))
⊢ (x ∈ piset(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{}x:coSet\{i:l\}.
    ((x  \mmember{}  piset(A;a.B[a]))
    \mLeftarrow{}{}\mRightarrow{}  \mexists{}f:t:set-dom(A)  {}\mrightarrow{}  set-dom(B[set-item(A;t)])
              \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)))))


By

---

Latex:
(Auto  THEN  ExRepD)

---

Home Index