---

Step * 1 1 of Lemma mset_mem_mon_for_union


1. s : DSet@i'
2. s' : DSet@i'
3. a : MSet{s}@i
4. e : |s| ⟶ MSet{s'}@i
5. x : |s'|@i
⊢ (λz.(x ∈b z)) (msFor{<MSet{s'},⋃,0>} y ∈ a. e[y]) = ∃b{s} y ∈ a. ((λz.(x ∈b z)) e[y])
BY
{ ((BLemma `dist_hom_over_mset_for`) THENA Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet@i'
2.  s'  :  DSet@i'
3.  a  :  MSet\{s\}@i
4.  e  :  |s|  {}\mrightarrow{}  MSet\{s'\}@i
5.  x  :  |s'|@i
\mvdash{}  (\mlambda{}z.(x  \mmember{}\msubb{}  z))  (msFor\{<MSet\{s'\},\mcup{},0>\}  y  \mmember{}  a.  e[y])  =  \mexists{}\msubb{}\{s\}  y  \mmember{}  a.  ((\mlambda{}z.(x  \mmember{}\msubb{}  z))  e[y])


By

---

Latex:
((BLemma  `dist\_hom\_over\_mset\_for`)  THENA  Auto)

---

Home Index