---

Step * 1 of Lemma bag-filter-same


1. T : Type
2. p : T ⟶ 𝔹
3. bs : bag(T)
4. ∀x:T. (x ↓∈ bs ⇒ (↑p[x]))
5. ∀[bs@0:bag({x:T| x ↓∈ bs} )]. ([x∈bs@0|p[x]] = bs@0 ∈ bag({x:T| x ↓∈ bs} ))
6. [x∈bs|p[x]] = bs ∈ bag({x:T| x ↓∈ bs} )
⊢ [x∈bs|p[x]] = bs ∈ bag(T)
BY
{ (HypSubst' -1 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  p  :  T  {}\mrightarrow{}  \mBbbB{}
3.  bs  :  bag(T)
4.  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  (\muparrow{}p[x]))
5.  \mforall{}[bs@0:bag(\{x:T|  x  \mdownarrow{}\mmember{}  bs\}  )].  ([x\mmember{}bs@0|p[x]]  =  bs@0)
6.  [x\mmember{}bs|p[x]]  =  bs
\mvdash{}  [x\mmember{}bs|p[x]]  =  bs


By

---

Latex:
(HypSubst'  -1  0  THEN  Auto)

---

Home Index