---

Step * of Lemma orderedpair-first

∀a,b:coSet{i:l}.  seteq(orderedpair-fsts((a,b));{a})
BY
{ (Unfold `orderedpair-fsts` 0 THEN Auto THEN Assert ⌜∃x:coSet{i:l}. (x ∈ (a,b))⌝⋅) }

1
.....assertion..... 
1. a : coSet{i:l}
2. b : coSet{i:l}
⊢ ∃x:coSet{i:l}. (x ∈ (a,b))

2
1. a : coSet{i:l}
2. b : coSet{i:l}
3. ∃x:coSet{i:l}. (x ∈ (a,b))
⊢ seteq(⋂((a,b));{a})

---

Latex:

---

Latex:
\mforall{}a,b:coSet\{i:l\}.    seteq(orderedpair-fsts((a,b));\{a\})


By

---

Latex:
(Unfold  `orderedpair-fsts`  0  THEN  Auto  THEN  Assert  \mkleeneopen{}\mexists{}x:coSet\{i:l\}.  (x  \mmember{}  (a,b))\mkleeneclose{}\mcdot{})

---

Home Index