---

Step * of Lemma mset_mem_mon_for_union

∀s,s':DSet. ∀a:MSet{s}. ∀e:|s| ⟶ MSet{s'}. ∀x:|s'|.  x ∈b msFor{<MSet{s'},⋃,0>} y ∈ a. e[y] = ∃b{s} y ∈ a. (x ∈b e[y])
BY
{ ((RepD) THENA Auto) }

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

---

Latex:

---

Latex:
\mforall{}s,s':DSet.  \mforall{}a:MSet\{s\}.  \mforall{}e:|s|  {}\mrightarrow{}  MSet\{s'\}.  \mforall{}x:|s'|.
    x  \mmember{}\msubb{}  msFor\{<MSet\{s'\},\mcup{},0>\}  y  \mmember{}  a.  e[y]  =  \mexists{}\msubb{}\{s\}  y  \mmember{}  a.  (x  \mmember{}\msubb{}  e[y])


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index