---

Step * of Lemma bag-member-filter-implies2

∀[T:Type]. ∀[x:T]. ∀[bs:bag(T)]. ∀[P:{x:T| x ↓∈ bs}  ⟶ 𝔹].  x ↓∈ bs ∧ (↑P[x]) supposing x ↓∈ [x∈bs|P[x]]
BY
{ TACTIC:(BasicUniformUnivCD Auto
          THEN Assert ⌜∀b1:T List. ∀x1:{x:T| x ↓∈ b1}  ⟶ 𝔹. ∀x:T.
                         (x ↓∈ [x∈b1|x1[x]] ⇒ ((Ax ∈ x ↓∈ b1) ∧ (Ax ∈ ↑x1[x])))⌝⋅
          ) }

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

2
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]]

---

Latex:

---

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


By

---

Latex:
TACTIC:(BasicUniformUnivCD  Auto
                THEN  Assert  \mkleeneopen{}\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])))\mkleeneclose{}\mcdot{}
                )

---

Home Index