---

Step * of Lemma bag-filter-is-empty

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[b:bag(T)].  uiff(∀x:T. (x ↓∈ b ⇒ (¬↑P[x]));[x∈b|P[x]] = {} ∈ bag(T))
BY
{ (InstLemma `bag-filter-empty-iff` [] THEN RepeatFor 4 (ParallelLast')) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. b : bag(T)
4. ∀x:T. (x ↓∈ b ⇒ (¬↑P[x]))
5. ↑bag-null([x∈b|P[x]])
⊢ [x∈b|P[x]] = {} ∈ bag(T)

2
.....antecedent..... 
1. T : Type
2. P : T ⟶ 𝔹
3. b : bag(T)
4. [x∈b|P[x]] = {} ∈ bag(T)
⊢ ↑bag-null([x∈b|P[x]])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[b:bag(T)].    uiff(\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (\mneg{}\muparrow{}P[x]));[x\mmember{}b|P[x]]  =  \{\})


By

---

Latex:
(InstLemma  `bag-filter-empty-iff`  []  THEN  RepeatFor  4  (ParallelLast'))

---

Home Index