---

Step * of Lemma orderedpair-snds_functionality

∀a,b:coSet{i:l}.  (seteq(a;b) ⇒ seteq(snds(a);snds(b)))
BY
{ (Auto THEN Unfold `orderedpair-snds` 0) }

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `orderedpair-snds`  0)

---

Home Index