---

Step * of Lemma orderedpair-second

∀a,b:coSet{i:l}.  seteq(snds((a,b));{b})
BY
{ (Auto THEN ((RWO "co-seteq-iff" 0 THENM D 0) THENA Auto) THEN Unfold `orderedpair-snds` 0) }

1
1. a : coSet{i:l}
2. b : coSet{i:l}
3. z : coSet{i:l}
⊢ (z ∈ {x ∈ ⋃((a,b)) | seteq((a,b);(fst((a,b)),x))}) ⇐⇒ (z ∈ {b})

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  ((RWO  "co-seteq-iff"  0  THENM  D  0)  THENA  Auto)  THEN  Unfold  `orderedpair-snds`  0)

---

Home Index