---

Step * 2 1 of Lemma bag-member-filter-implies2


1. T : Type
2. x : T
3. bs : bag(T)
4. P : {x:T| x ↓∈ bs}  ⟶ 𝔹
5. ∀b1:T List. ∀x1:{x:T| x ↓∈ b1}  ⟶ 𝔹. ∀x:T.  (x ↓∈ [x∈b1|x1[x]] ⇒ ((Ax ∈ x ↓∈ b1) ∧ (Ax ∈ ↑x1[x])))
⊢ x ↓∈ bs ∧ (↑P[x]) supposing x ↓∈ [x∈bs|P[x]]
BY
{ (MoveToConcl (-2)⋅ THEN UseWitness ⌜λp.<Ax, Ax>⌝⋅) }

1
1. T : Type
2. x : T
3. bs : bag(T)
4. ∀b1:T List. ∀x1:{x:T| x ↓∈ b1}  ⟶ 𝔹. ∀x:T.  (x ↓∈ [x∈b1|x1[x]] ⇒ ((Ax ∈ x ↓∈ b1) ∧ (Ax ∈ ↑x1[x])))
⊢ λp.<Ax, Ax> ∈ ∀P:{x:T| x ↓∈ bs}  ⟶ 𝔹. x ↓∈ bs ∧ (↑P[x]) supposing x ↓∈ [x∈bs|P[x]]

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  bs  :  bag(T)
4.  P  :  \{x:T|  x  \mdownarrow{}\mmember{}  bs\}    {}\mrightarrow{}  \mBbbB{}
5.  \mforall{}b1:T  List.  \mforall{}x1:\{x:T|  x  \mdownarrow{}\mmember{}  b1\}    {}\mrightarrow{}  \mBbbB{}.  \mforall{}x:T.
          (x  \mdownarrow{}\mmember{}  [x\mmember{}b1|x1[x]]  {}\mRightarrow{}  ((Ax  \mmember{}  x  \mdownarrow{}\mmember{}  b1)  \mwedge{}  (Ax  \mmember{}  \muparrow{}x1[x])))
\mvdash{}  x  \mdownarrow{}\mmember{}  bs  \mwedge{}  (\muparrow{}P[x])  supposing  x  \mdownarrow{}\mmember{}  [x\mmember{}bs|P[x]]


By

---

Latex:
(MoveToConcl  (-2)\mcdot{}  THEN  UseWitness  \mkleeneopen{}\mlambda{}p.<Ax,  Ax>\mkleeneclose{}\mcdot{})

---

Home Index