---

Step * 1 1 of Lemma seteq-orderedpairs-iff


1. a : coSet{i:l}
2. b : coSet{i:l}
3. a' : coSet{i:l}
4. b' : coSet{i:l}
5. ∀z:coSet{i:l}. (seteq(z;{a}) ∨ seteq(z;{a,b}) ⇐⇒ seteq(z;{a'}) ∨ seteq(z;{a',b'}))
⊢ seteq(a;a') ∧ seteq(b;b')
BY
{ (Assert seteq(a;a') BY
         ((InstHyp [⌜{a}⌝] (-1)⋅ THENA Auto)
          THEN D -1
          THEN (D -2 THENA (Auto THEN OrLeft THEN Try (RelRST) THEN Auto))
          THEN D -1
          THEN (RWO "co-seteq-iff" (-1) THENA Auto)
          THEN (RWO "setmem-pairset setmem-singleset" (-1)⋅ THENA Auto)
          THEN Try ((BHyp -1  THEN Complete (Auto)))
          THEN (InstHyp [⌜a'⌝] (-1)⋅ THENA Auto)
          THEN RepeatFor 2 (D -1)
          THEN Auto)) }

1
1. a : coSet{i:l}
2. b : coSet{i:l}
3. a' : coSet{i:l}
4. b' : coSet{i:l}
5. ∀z:coSet{i:l}. (seteq(z;{a}) ∨ seteq(z;{a,b}) ⇐⇒ seteq(z;{a'}) ∨ seteq(z;{a',b'}))
6. seteq(a;a')
⊢ seteq(a;a') ∧ seteq(b;b')

---

Latex:

---

Latex:

1.  a  :  coSet\{i:l\}
2.  b  :  coSet\{i:l\}
3.  a'  :  coSet\{i:l\}
4.  b'  :  coSet\{i:l\}
5.  \mforall{}z:coSet\{i:l\}.  (seteq(z;\{a\})  \mvee{}  seteq(z;\{a,b\})  \mLeftarrow{}{}\mRightarrow{}  seteq(z;\{a'\})  \mvee{}  seteq(z;\{a',b'\}))
\mvdash{}  seteq(a;a')  \mwedge{}  seteq(b;b')


By

---

Latex:
(Assert  seteq(a;a')  BY
              ((InstHyp  [\mkleeneopen{}\{a\}\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                THEN  D  -1
                THEN  (D  -2  THENA  (Auto  THEN  OrLeft  THEN  Try  (RelRST)  THEN  Auto))
                THEN  D  -1
                THEN  (RWO  "co-seteq-iff"  (-1)  THENA  Auto)
                THEN  (RWO  "setmem-pairset  setmem-singleset"  (-1)\mcdot{}  THENA  Auto)
                THEN  Try  ((BHyp  -1    THEN  Complete  (Auto)))
                THEN  (InstHyp  [\mkleeneopen{}a'\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                THEN  RepeatFor  2  (D  -1)
                THEN  Auto))

---

Home Index