---

Step * of Lemma setmem-productset

∀a,b,p:coSet{i:l}.  ((p ∈ a x b) ⇐⇒ ∃u,v:coSet{i:l}. ((u ∈ a) ∧ (v ∈ b) ∧ seteq(p;(u,v))))
BY
{ (RepeatFor 2 ((Intro THEN coSetD (-1)⋅ THEN D -1)) THEN Auto) }

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. (p ∈ <T, a1> x <T1, b1>)
⊢ ∃u,v:coSet{i:l}. ((u ∈ <T, a1>) ∧ (v ∈ <T1, b1>) ∧ seteq(p;(u,v)))

2
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>)

---

Latex:

---

Latex:
\mforall{}a,b,p:coSet\{i:l\}.    ((p  \mmember{}  a  x  b)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}u,v:coSet\{i:l\}.  ((u  \mmember{}  a)  \mwedge{}  (v  \mmember{}  b)  \mwedge{}  seteq(p;(u,v))))


By

---

Latex:
(RepeatFor  2  ((Intro  THEN  coSetD  (-1)\mcdot{}  THEN  D  -1))  THEN  Auto)

---

Home Index