---

Step * 2 of Lemma setmem-productset


1. T : Type
2. a1 : T ⟶ coSet{i:l}
3. T1 : Type
4. b1 : T1 ⟶ coSet{i:l}
5. p : coSet{i:l}
6. ∃u,v:coSet{i:l}. ((u ∈ <T, a1>) ∧ (v ∈ <T1, b1>) ∧ seteq(p;(u,v)))
⊢ (p ∈ <T, a1> x <T1, b1>)
BY
{ (All (Fold `mk-coset`) THEN ExRepD THEN All SetMemDef THEN D 0 With ⌜<t1, t>⌝  THEN Auto THEN Reduce 0) }

1
1. T : Type
2. a1 : T ⟶ coSet{i:l}
3. T1 : Type
4. b1 : T1 ⟶ coSet{i:l}
5. p : coSet{i:l}
6. u : coSet{i:l}
7. v : coSet{i:l}
8. t1 : T
9. seteq(u;a1 t1)
10. t : T1
11. seteq(v;b1 t)
12. seteq(p;(u,v))
⊢ seteq(p;(a1 t1,b1 t))

---

Latex:

---

Latex:

1.  T  :  Type
2.  a1  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  T1  :  Type
4.  b1  :  T1  {}\mrightarrow{}  coSet\{i:l\}
5.  p  :  coSet\{i:l\}
6.  \mexists{}u,v:coSet\{i:l\}.  ((u  \mmember{}  <T,  a1>)  \mwedge{}  (v  \mmember{}  <T1,  b1>)  \mwedge{}  seteq(p;(u,v)))
\mvdash{}  (p  \mmember{}  <T,  a1>  x  <T1,  b1>)


By

---

Latex:
(All  (Fold  `mk-coset`)  THEN  ExRepD  THEN  All  SetMemDef  THEN  D  0  With  \mkleeneopen{}<t1,  t>\mkleeneclose{}    THEN  Auto  THEN  Reduce\000C  0)

---

Home Index