---

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


1. [T] : Type
2. b1 : T List
3. x1 : {x:T| x ↓∈ b1}  ⟶ 𝔹
4. x : T
5. x ↓∈ [x∈b1|x1[x]]
⊢ (Ax ∈ x ↓∈ b1) ∧ (Ax ∈ ↑x1[x])
BY
{ D 0 }

1
1. [T] : Type
2. b1 : T List
3. x1 : {x:T| x ↓∈ b1}  ⟶ 𝔹
4. x : T
5. x ↓∈ [x∈b1|x1[x]]
⊢ Ax ∈ x ↓∈ b1

2
1. [T] : Type
2. b1 : T List
3. x1 : {x:T| x ↓∈ b1}  ⟶ 𝔹
4. x : T
5. x ↓∈ [x∈b1|x1[x]]
⊢ Ax ∈ ↑x1[x]

---

Latex:

---

Latex:

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


By

---

Latex:
D  0

---

Home Index