---

Step * 1 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'}))
6. seteq(a;a')
⊢ seteq(a;a') ∧ seteq(b;b')
BY
{ (Auto
   THEN (InstHyp [⌜{a,b}⌝] (-3)⋅ THENA Auto)
   THEN D -1
   THEN (D -2 THENA Auto)
   THEN D -1
   THEN (RWO "co-seteq-iff" (-1) THENA Auto)
   THEN (RWO "setmem-pairset setmem-singleset" (-1)⋅ THENA Auto)
   THEN (InstHyp [⌜b⌝] (-1)⋅ THENA Auto)
   THEN D -1
   THEN (D -2 THENA Auto)
   THEN ((D -1 THEN Auto) ORELSE (Assert seteq(b;a) BY Auto))
   THEN (InstHyp [⌜{a',b'}⌝] 5⋅ THENA Auto)
   THEN (RepeatFor 2 (D -1) THENA Auto)
   THEN D -1
   THEN (RWO "co-seteq-iff" (-1) THENA Auto)
   THEN (RWO "setmem-pairset setmem-singleset" (-1)⋅ THENA Auto)
   THEN (InstHyp [⌜b'⌝] (-1)⋅ THENA Auto)
   THEN D -1
   THEN D -2
   THEN Auto
   THEN D -1
   THEN Auto) }

---

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'\}))
6.  seteq(a;a')
\mvdash{}  seteq(a;a')  \mwedge{}  seteq(b;b')


By

---

Latex:
(Auto
  THEN  (InstHyp  [\mkleeneopen{}\{a,b\}\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (D  -2  THENA  Auto)
  THEN  D  -1
  THEN  (RWO  "co-seteq-iff"  (-1)  THENA  Auto)
  THEN  (RWO  "setmem-pairset  setmem-singleset"  (-1)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (D  -2  THENA  Auto)
  THEN  ((D  -1  THEN  Auto)  ORELSE  (Assert  seteq(b;a)  BY  Auto))
  THEN  (InstHyp  [\mkleeneopen{}\{a',b'\}\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  (RepeatFor  2  (D  -1)  THENA  Auto)
  THEN  D  -1
  THEN  (RWO  "co-seteq-iff"  (-1)  THENA  Auto)
  THEN  (RWO  "setmem-pairset  setmem-singleset"  (-1)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}b'\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  D  -2
  THEN  Auto
  THEN  D  -1
  THEN  Auto)

---

Home Index