---

Step * of Lemma sv-bag-only-filter

∀[A:Type]. ∀[b:bag(A)]. ∀[p:{x:A| x ↓∈ b}  ⟶ 𝔹].
  ∀x:A. (sv-bag-only([x∈b|p[x]]) = x ∈ A) supposing ((↑p[x]) and x ↓∈ b and (∀y:A. (y ↓∈ b ⇒ (↑p[y]) ⇒ (y = x ∈ A))))
BY
{ (Auto
   THEN (Assert ⌜[x∈b|p[x]] ∈ bag(A)⌝⋅ THENA (InstLemma `bag-filter-wf2` [⌜A⌝;⌜b⌝;⌜p⌝]⋅ THEN Auto))
   THEN (Assert ⌜single-valued-bag([x∈b|p[x]];A)⌝⋅
         THENA (BLemma `single-valued-bag-filter`
                THEN Auto
                THEN (InstHyp [⌜y⌝] (-10)⋅ THENA Auto)
                THEN InstHyp [⌜x1⌝] (-11)⋅
                THEN Auto)
         )
   THEN (Assert ⌜0 < #([x∈b|p[x]])⌝⋅
         THENA (Using [`x',⌜x⌝] (BLemma `bag-member-size`)⋅ THEN Auto THEN RWO "bag-member-filter2" 0 THEN Auto)
         )
   THEN (InstLemma `bag-member-sv-bag-only` [⌜A⌝;⌜[x∈b|p[x]]⌝]⋅ THENA Auto)
   THEN (RWO "bag-member-filter2" (-1) THENA Auto)
   THEN Auto
   THEN Unfold `single-valued-bag` (-6)
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[b:bag(A)].  \mforall{}[p:\{x:A|  x  \mdownarrow{}\mmember{}  b\}    {}\mrightarrow{}  \mBbbB{}].
    \mforall{}x:A
        (sv-bag-only([x\mmember{}b|p[x]])  =  x)  supposing 
              ((\muparrow{}p[x])  and 
              x  \mdownarrow{}\mmember{}  b  and 
              (\mforall{}y:A.  (y  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (\muparrow{}p[y])  {}\mRightarrow{}  (y  =  x))))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}[x\mmember{}b|p[x]]  \mmember{}  bag(A)\mkleeneclose{}\mcdot{}  THENA  (InstLemma  `bag-filter-wf2`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}single-valued-bag([x\mmember{}b|p[x]];A)\mkleeneclose{}\mcdot{}
              THENA  (BLemma  `single-valued-bag-filter`
                            THEN  Auto
                            THEN  (InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  (-10)\mcdot{}  THENA  Auto)
                            THEN  InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  (-11)\mcdot{}
                            THEN  Auto)
              )
  THEN  (Assert  \mkleeneopen{}0  <  \#([x\mmember{}b|p[x]])\mkleeneclose{}\mcdot{}
              THENA  (Using  [`x',\mkleeneopen{}x\mkleeneclose{}]  (BLemma  `bag-member-size`)\mcdot{}
                            THEN  Auto
                            THEN  RWO  "bag-member-filter2"  0
                            THEN  Auto)
              )
  THEN  (InstLemma  `bag-member-sv-bag-only`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}[x\mmember{}b|p[x]]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "bag-member-filter2"  (-1)  THENA  Auto)
  THEN  Auto
  THEN  Unfold  `single-valued-bag`  (-6)
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index