---

Step * 1 1 1 1 1 1 1 of Lemma implies-setmem-piset


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. g : ∀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))
9. m : ∀t:set-dom(A). (set-item(A;t) ∈ A)
10. λt.(fst((g set-item(A;t) (m t)))) ∈ t:set-dom(A) ⟶ coSet{i:l}
11. λt.(snd((g set-item(A;t) (m t)))) ∈ t:set-dom(A) ⟶ ((fst((g set-item(A;t) (m t))) ∈ B[set-item(A;t)])
                                                        ∧ ((set-item(A;t),fst((g set-item(A;t) (m t)))) ∈ x))
12. λt.(fst(snd((g set-item(A;t) (m t))))) ∈ t:set-dom(A) ⟶ (fst((g set-item(A;t) (m t))) ∈ B[set-item(A;t)])
13. λt.(fst(((λt.(fst(snd((g set-item(A;t) (m t)))))) t))) ∈ t:set-dom(A) ⟶ set-dom(B[set-item(A;t)])
14. z : coSet{i:l}
15. (z ∈ x)
16. a : coSet{i:l}
17. (a ∈ A)
18. b : coSet{i:l}
19. (b ∈ B[a])
20. seteq(z;(a,b))
⊢ ∃t:set-dom(A)
   seteq(z;(set-item(A;t),set-item(B[set-item(A;t)];(λt.(fst(((λt.(fst(snd((g set-item(A;t) (m t)))))) t)))) t)))
BY
{ (((coSetD 1 THEN D 1 THEN All (Fold `mk-coset`)) THEN SetMemDef (-4)) THEN Reduce 0) }

1
1. T : Type
2. A1 : T ⟶ coSet{i:l}
3. ∀t:set-dom(mk-coset(T;A1)). (set-item(mk-coset(T;A1);t) ∈ {a:coSet{i:l}| (a ∈ mk-coset(T;A1))} )
4. B : {a:coSet{i:l}| (a ∈ mk-coset(T;A1))}  ⟶ coSet{i:l}
5. x : coSet{i:l}
6. ∀a1,a2:coSet{i:l}.  ((a1 ∈ mk-coset(T;A1)) ⇒ (a2 ∈ mk-coset(T;A1)) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2]))
7. (x ⊆ Σa:mk-coset(T;A1).B[a])
8. g : ∀a:coSet{i:l}. ((a ∈ mk-coset(T;A1)) ⇒ (∃b:coSet{i:l}. ((b ∈ B[a]) ∧ ((a,b) ∈ x))))
9. ∀a,b1,b2:coSet{i:l}.
     ((a ∈ mk-coset(T;A1)) ⇒ (b1 ∈ B[a]) ⇒ (b2 ∈ B[a]) ⇒ ((a,b1) ∈ x) ⇒ ((a,b2) ∈ x) ⇒ seteq(b1;b2))
10. m : ∀t:set-dom(mk-coset(T;A1)). (set-item(mk-coset(T;A1);t) ∈ mk-coset(T;A1))
11. λt.(fst((g set-item(mk-coset(T;A1);t) (m t)))) ∈ t:set-dom(mk-coset(T;A1)) ⟶ coSet{i:l}
12. λt.(snd((g set-item(mk-coset(T;A1);t) (m t)))) ∈ t:set-dom(mk-coset(T;A1))
    ⟶ ((fst((g set-item(mk-coset(T;A1);t) (m t))) ∈ B[set-item(mk-coset(T;A1);t)])
       ∧ ((set-item(mk-coset(T;A1);t),fst((g set-item(mk-coset(T;A1);t) (m t)))) ∈ x))
13. λt.(fst(snd((g set-item(mk-coset(T;A1);t) (m t))))) ∈ t:set-dom(mk-coset(T;A1))
    ⟶ (fst((g set-item(mk-coset(T;A1);t) (m t))) ∈ B[set-item(mk-coset(T;A1);t)])
14. λt.(fst(((λt.(fst(snd((g set-item(mk-coset(T;A1);t) (m t)))))) t))) ∈ t:set-dom(mk-coset(T;A1))
    ⟶ set-dom(B[set-item(mk-coset(T;A1);t)])
15. z : coSet{i:l}
16. (z ∈ x)
17. a : coSet{i:l}
18. t : T
19. seteq(a;A1 t)
20. b : coSet{i:l}
21. (b ∈ B[a])
22. seteq(z;(a,b))
⊢ ∃t:set-dom(mk-coset(T;A1))
   seteq(z;(set-item(mk-coset(T;A1);t),set-item(B[set-item(mk-coset(T;A1);t)];fst(fst(snd((g set-item(mk-coset(T;A1);t) 
                                                                                           (m 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.  (x  \msubseteq{}  \mSigma{}a:A.B[a])
7.  g  :  \mforall{}a:coSet\{i:l\}.  ((a  \mmember{}  A)  {}\mRightarrow{}  (\mexists{}b:coSet\{i:l\}.  ((b  \mmember{}  B[a])  \mwedge{}  ((a,b)  \mmember{}  x))))
8.  \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))
9.  m  :  \mforall{}t:set-dom(A).  (set-item(A;t)  \mmember{}  A)
10.  \mlambda{}t.(fst((g  set-item(A;t)  (m  t))))  \mmember{}  t:set-dom(A)  {}\mrightarrow{}  coSet\{i:l\}
11.  \mlambda{}t.(snd((g  set-item(A;t)  (m  t))))  \mmember{}  t:set-dom(A)
        {}\mrightarrow{}  ((fst((g  set-item(A;t)  (m  t)))  \mmember{}  B[set-item(A;t)])
              \mwedge{}  ((set-item(A;t),fst((g  set-item(A;t)  (m  t))))  \mmember{}  x))
12.  \mlambda{}t.(fst(snd((g  set-item(A;t)  (m  t)))))  \mmember{}  t:set-dom(A)
        {}\mrightarrow{}  (fst((g  set-item(A;t)  (m  t)))  \mmember{}  B[set-item(A;t)])
13.  \mlambda{}t.(fst(((\mlambda{}t.(fst(snd((g  set-item(A;t)  (m  t))))))  t)))  \mmember{}  t:set-dom(A)
        {}\mrightarrow{}  set-dom(B[set-item(A;t)])
14.  z  :  coSet\{i:l\}
15.  (z  \mmember{}  x)
16.  a  :  coSet\{i:l\}
17.  (a  \mmember{}  A)
18.  b  :  coSet\{i:l\}
19.  (b  \mmember{}  B[a])
20.  seteq(z;(a,b))
\mvdash{}  \mexists{}t:set-dom(A)
      seteq(z;(set-item(A;t),set-item(B[set-item(A;t)];(\mlambda{}t.(fst(((\mlambda{}t.(fst(snd((g  set-item(A;t) 
                                                                                                                                                        (m  t)))))) 
                                                                                                                            t)))) 
                                                                                                        t)))


By

---

Latex:
(((coSetD  1  THEN  D  1  THEN  All  (Fold  `mk-coset`))  THEN  SetMemDef  (-4))  THEN  Reduce  0)

---

Home Index