---

Step * 1 1 1 of Lemma omral_dom_action


1. g : OCMon
2. r : CDRng
3. v : |r|
4. ps : |omral(g;r)|
5. x : |(g↓oset)|
6. ↑(x
∈b fs-map(λk'.(k' * e), dom(ps)))
⊢ ↑(x
∈b dom(ps))
BY
{ ((RWW "u:fset_map fset_of_mset_mem" 6) THENA Auto) }

1
1. g : OCMon
2. r : CDRng
3. v : |r|
4. ps : |omral(g;r)|
5. x : |(g↓oset)|
6. ↑(x
∈b msmap{g↓oset,g↓oset}(λk'.(k' * e);dom(ps)))
⊢ ↑(x
∈b dom(ps))

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  v  :  |r|
4.  ps  :  |omral(g;r)|
5.  x  :  |(g\mdownarrow{}oset)|
6.  \muparrow{}(x
\mmember{}\msubb{}  fs-map(\mlambda{}k'.(k'  *  e),  dom(ps)))
\mvdash{}  \muparrow{}(x
\mmember{}\msubb{}  dom(ps))


By

---

Latex:
((RWW  "u:fset\_map  fset\_of\_mset\_mem"  6)  THENA  Auto)

---

Home Index