---

Step * 1 1 of Lemma bag-combine-filter


1. A : Type
2. B : Type
3. p : A ⟶ 𝔹
4. f : {a:A| ↑p[a]}  ⟶ bag(B)
5. as : A List
6. bs : A List
7. permutation(A;as;bs)
8. as = bs ∈ bag(A)
9. as ∈ bag(A)
10. bs ∈ bag(A)
⊢ ⋃a∈[a∈as|p[a]].f[a] = ⋃a∈bs.if p[a] then f[a] else {} fi  ∈ bag(B)
BY
{ Subst ⌜⋃a∈[a∈as|p[a]].f[a] = ⋃a∈as.if p[a] then f[a] else {} fi  ∈ bag(B)⌝ 0⋅ }

1
.....equality..... 
1. A : Type
2. B : Type
3. p : A ⟶ 𝔹
4. f : {a:A| ↑p[a]}  ⟶ bag(B)
5. as : A List
6. bs : A List
7. permutation(A;as;bs)
8. as = bs ∈ bag(A)
9. as ∈ bag(A)
10. bs ∈ bag(A)
⊢ ⋃a∈[a∈as|p[a]].f[a] = ⋃a∈as.if p[a] then f[a] else {} fi  ∈ bag(B)

2
1. A : Type
2. B : Type
3. p : A ⟶ 𝔹
4. f : {a:A| ↑p[a]}  ⟶ bag(B)
5. as : A List
6. bs : A List
7. permutation(A;as;bs)
8. as = bs ∈ bag(A)
9. as ∈ bag(A)
10. bs ∈ bag(A)
⊢ ⋃a∈as.if p[a] then f[a] else {} fi  = ⋃a∈bs.if p[a] then f[a] else {} fi  ∈ bag(B)

3
.....wf..... 
1. A : Type
2. B : Type
3. p : A ⟶ 𝔹
4. f : {a:A| ↑p[a]}  ⟶ bag(B)
5. as : A List
6. bs : A List
7. permutation(A;as;bs)
8. as = bs ∈ bag(A)
9. as ∈ bag(A)
10. bs ∈ bag(A)
11. z : bag(B)
⊢ z = ⋃a∈bs.if p[a] then f[a] else {} fi  ∈ bag(B) ∈ ℙ

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  p  :  A  {}\mrightarrow{}  \mBbbB{}
4.  f  :  \{a:A|  \muparrow{}p[a]\}    {}\mrightarrow{}  bag(B)
5.  as  :  A  List
6.  bs  :  A  List
7.  permutation(A;as;bs)
8.  as  =  bs
9.  as  \mmember{}  bag(A)
10.  bs  \mmember{}  bag(A)
\mvdash{}  \mcup{}a\mmember{}[a\mmember{}as|p[a]].f[a]  =  \mcup{}a\mmember{}bs.if  p[a]  then  f[a]  else  \{\}  fi 


By

---

Latex:
Subst  \mkleeneopen{}\mcup{}a\mmember{}[a\mmember{}as|p[a]].f[a]  =  \mcup{}a\mmember{}as.if  p[a]  then  f[a]  else  \{\}  fi  \mkleeneclose{}  0\mcdot{}

---

Home Index