---

Step * of Lemma classfun-res-parallel-class-left

∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(A)]. ∀[e:E].
  (X || Y@e ~ X@e) supposing (disjoint-classrel(es;A;X;A;Y) and (↑e ∈b X))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``parallel-class eclass-compose2 classfun-res classfun`` 0
   THEN (Assert ⌜Y es e ~ {}⌝⋅ THENM (HypSubst' (-1) 0 THEN RWO "bag-append-empty" 0 THEN Auto))
   THEN All (RepUR ``disjoint-classrel``)
   THEN (InstHyp [⌜e⌝] (-1)⋅ THENA Auto)
   THEN D (-1)
   THEN Try (Complete (((Assert ⌜False⌝⋅ THEN Auto)
                        THEN (FLemma `assert-member-eclass` [-3] THENA Auto)
                        THEN SquashExRepD
                        THEN InstHyp [⌜v⌝] (-3)⋅
                        THEN Auto)))
   THEN RepUR ``classrel`` (-1)
   THEN (RWO "empty-bag-iff-no-member<" (-1) THENA Auto)
   THEN BLemma `equal-empty-bag`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(A)].  \mforall{}[e:E].
    (X  ||  Y@e  \msim{}  X@e)  supposing  (disjoint-classrel(es;A;X;A;Y)  and  (\muparrow{}e  \mmember{}\msubb{}  X))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``parallel-class  eclass-compose2  classfun-res  classfun``  0
  THEN  (Assert  \mkleeneopen{}Y  es  e  \msim{}  \{\}\mkleeneclose{}\mcdot{}  THENM  (HypSubst'  (-1)  0  THEN  RWO  "bag-append-empty"  0  THEN  Auto))
  THEN  All  (RepUR  ``disjoint-classrel``)
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Try  (Complete  (((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
                                            THEN  (FLemma  `assert-member-eclass`  [-3]  THENA  Auto)
                                            THEN  SquashExRepD
                                            THEN  InstHyp  [\mkleeneopen{}v\mkleeneclose{}]  (-3)\mcdot{}
                                            THEN  Auto)))
  THEN  RepUR  ``classrel``  (-1)
  THEN  (RWO  "empty-bag-iff-no-member<"  (-1)  THENA  Auto)
  THEN  BLemma  `equal-empty-bag`
  THEN  Auto)

---

Home Index