---

Step * of Lemma setmem-Piset

∀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]) ⇐⇒ function-graph{i:l}(A;a.B[a];x)))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `Piset` 0
   THEN (RWO "setmem-sub-coset" 0 THENA Auto)
   THEN RepeatFor 2 ((D 0 THENA Auto))) }

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

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

---

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\}.
    ((\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  \mmember{}  \mPi{}a:A.B[a])  \mLeftarrow{}{}\mRightarrow{}  function-graph\{i:l\}(A;a.B[a];x)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `Piset`  0
  THEN  (RWO  "setmem-sub-coset"  0  THENA  Auto)
  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index