---

Step * of Lemma single-valued-bag-filter

∀[A:Type]. ∀[b:bag(A)]. ∀[p:{x:A| x ↓∈ b}  ⟶ 𝔹].
  single-valued-bag([x∈b|p[x]];A) supposing ∀x,y:A.  (x ↓∈ b ⇒ y ↓∈ b ⇒ (↑p[x]) ⇒ (↑p[y]) ⇒ (x = y ∈ A))
BY
{ (((UnivCD THENM (Unfold `single-valued-bag` 0 THEN UnivCD))
    THENA (Try (InstLemma `bag-filter-wf2` [⌜A⌝;⌜b⌝;⌜p⌝]⋅) THEN Auto)
    )
   THEN BackThruSomeHyp
   THEN Try (Complete ((RWO "bag-member-filter2" (-2) THEN Auto)))
   THEN Try (Complete ((RWO "bag-member-filter2" (-1) THEN Auto)))) }

---

Latex:

---

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


By

---

Latex:
(((UnivCD  THENM  (Unfold  `single-valued-bag`  0  THEN  UnivCD))
    THENA  (Try  (InstLemma  `bag-filter-wf2`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{})  THEN  Auto)
    )
  THEN  BackThruSomeHyp
  THEN  Try  (Complete  ((RWO  "bag-member-filter2"  (-2)  THEN  Auto)))
  THEN  Try  (Complete  ((RWO  "bag-member-filter2"  (-1)  THEN  Auto))))

---

Home Index