---

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


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]]
BY
{ TACTIC:BagD 3 }

1
.....wf..... 
1. T : Type
2. x : T
3. bs : as,bs:T List//permutation(T;as;bs)
4. ∀b1:T List. ∀x1:{x:T| x ↓∈ b1}  ⟶ 𝔹. ∀x:T.  (x ↓∈ [x∈b1|x1[x]] ⇒ ((Ax ∈ x ↓∈ b1) ∧ (Ax ∈ ↑x1[x])))
⊢ ∀P:{x:T| x ↓∈ bs}  ⟶ 𝔹. x ↓∈ bs ∧ (↑P[x]) supposing x ↓∈ [x∈bs|P[x]] ∈ Type

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  bs  :  bag(T)
4.  \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{}  \mlambda{}p.<Ax,  Ax>  \mmember{}  \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:BagD  3

---

Home Index