---

Step * of Lemma bag-member-filter-set

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[x:{x:T| ↑P[x]} ]. ∀[bs:bag(T)].  uiff(x ↓∈ [x∈bs|P[x]];x ↓∈ bs)
BY
{ (Auto
   THEN DVar `x'
   THEN (Unhide THEN Auto)
   THEN Try (((InstLemma `bag-member-subtype` [⌜{x:T| ↑P[x]} ⌝;⌜T⌝]⋅ THENA (Auto THEN SubtypeReasoning THEN Auto))
              THEN (FHyp (-1) [-2] THEN Auto)
              THEN BagMemberD (-1)
              THEN Auto))) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. x : T
4. ↑P[x]
5. bs : bag(T)
6. x ↓∈ [x∈bs|P[x]]
⊢ x ↓∈ bs

2
1. T : Type
2. P : T ⟶ 𝔹
3. x : T
4. ↑P[x]
5. bs : bag(T)
6. x ↓∈ bs
⊢ x ↓∈ [x∈bs|P[x]]

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  DVar  `x'
  THEN  (Unhide  THEN  Auto)
  THEN  Try  (((InstLemma  `bag-member-subtype`  [\mkleeneopen{}\{x:T|  \muparrow{}P[x]\}  \mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}
                          THENA  (Auto  THEN  SubtypeReasoning  THEN  Auto)
                          )
                        THEN  (FHyp  (-1)  [-2]  THEN  Auto)
                        THEN  BagMemberD  (-1)
                        THEN  Auto)))

---

Home Index