---

Step * of Lemma member-eclass-simple-comb-1

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[F:bag(A) ─→ bag(B)]. ∀[X:EClass(A)].
  (↑e ∈b F|X|) supposing ((∀as:bag(A). ((¬↑bag-null(as)) ⇒ (¬↑bag-null(F as)))) and (↑e ∈b X))
BY
{ ((UnivCD THENA Auto)
   THEN (InstHyp [⌈X es e⌉] (-1)⋅
         THENA (Auto
                THEN (D 0 THENA Auto)
                THEN (FLemma `assert-bag-null-sq` [-1] THENA (Auto THEN DoSubsume THEN Auto))
                THEN (RWO "member-eclass-iff-size" (-4) THENA Auto)
                THEN RWO "-1" (-4)
                THEN Reduce (-4)
                THEN Auto)
         )
   THEN All (RepUR ``simple-comb-1 simple-comb member-eclass``)⋅
   THEN (RWO "null-bag-size<" 0 THENA Auto)
   THEN (RWO "null-bag-size<" (-3) THENA Auto)
   THEN Repeat (AllPushDown)
   THEN BackThruSomeHyp) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[F:bag(A)  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].
    (\muparrow{}e  \mmember{}\msubb{}  F|X|)  supposing  ((\mforall{}as:bag(A).  ((\mneg{}\muparrow{}bag-null(as))  {}\mRightarrow{}  (\mneg{}\muparrow{}bag-null(F  as))))  and  (\muparrow{}e  \mmember{}\msubb{}  X))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}X  es  e\mkleeneclose{}]  (-1)\mcdot{}
              THENA  (Auto
                            THEN  (D  0  THENA  Auto)
                            THEN  (FLemma  `assert-bag-null-sq`  [-1]  THENA  (Auto  THEN  DoSubsume  THEN  Auto))
                            THEN  (RWO  "member-eclass-iff-size"  (-4)  THENA  Auto)
                            THEN  RWO  "-1"  (-4)
                            THEN  Reduce  (-4)
                            THEN  Auto)
              )
  THEN  All  (RepUR  ``simple-comb-1  simple-comb  member-eclass``)\mcdot{}
  THEN  (RWO  "null-bag-size<"  0  THENA  Auto)
  THEN  (RWO  "null-bag-size<"  (-3)  THENA  Auto)
  THEN  Repeat  (AllPushDown)
  THEN  BackThruSomeHyp)

---

Home Index