---

Step * 1 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. (p ∈ <T, a1> x <T1, b1>)
⊢ ∃u,v:coSet{i:l}. ((u ∈ <T, a1>) ∧ (v ∈ <T1, b1>) ∧ seteq(p;(u,v)))
BY
{ (SetMemDef (-1) THEN D -2 THEN All Reduce THEN InstConcl [⌜a1 t1⌝;⌜b1 t2⌝]⋅ THEN Auto) }

---

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.  (p  \mmember{}  <T,  a1>  x  <T1,  b1>)
\mvdash{}  \mexists{}u,v:coSet\{i:l\}.  ((u  \mmember{}  <T,  a1>)  \mwedge{}  (v  \mmember{}  <T1,  b1>)  \mwedge{}  seteq(p;(u,v)))


By

---

Latex:
(SetMemDef  (-1)  THEN  D  -2  THEN  All  Reduce  THEN  InstConcl  [\mkleeneopen{}a1  t1\mkleeneclose{};\mkleeneopen{}b1  t2\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index