---

Step * 1 of Lemma eo-restrict-restrict


1. es : EO
2. P : E ─→ 𝔹
3. Q : {e:E| ↑(P e)}  ─→ 𝔹
⊢ es["dom" := λe.((es."dom" e) ∧b (P e))]["dom" := λe.(((es."dom" e) ∧b (P e)) ∧b (Q e))]
= es["dom" := λe.((es."dom" e) ∧b (P e) ∧b (Q e))]
∈ EO
BY
{ (Fold `es-dom` 0
   THEN AllHyps h.(Unfold `es-E` h THEN Folds ``es-base-E es-dom`` h) 
   THEN (Fold `eo-reset-dom` 0 THEN RWO  "eo-reset-dom-reset-dom" 0)
   THEN (RWW "band_assoc" 0 THEN Auto)⋅) }

---

Latex:



1.  es  :  EO
2.  P  :  E  {}\mrightarrow{}  \mBbbB{}
3.  Q  :  \{e:E|  \muparrow{}(P  e)\}    {}\mrightarrow{}  \mBbbB{}
\mvdash{}  es["dom"  :=  \mlambda{}e.((es."dom"  e)  \mwedge{}\msubb{}  (P  e))]["dom"  :=  \mlambda{}e.(((es."dom"  e)  \mwedge{}\msubb{}  (P  e))  \mwedge{}\msubb{}  (Q  e))]
=  es["dom"  :=  \mlambda{}e.((es."dom"  e)  \mwedge{}\msubb{}  (P  e)  \mwedge{}\msubb{}  (Q  e))]


By

(Fold  `es-dom`  0
  THEN  AllHyps  h.(Unfold  `es-E`  h  THEN  Folds  ``es-base-E  es-dom``  h) 
  THEN  (Fold  `eo-reset-dom`  0  THEN  RWO    "eo-reset-dom-reset-dom"  0)
  THEN  (RWW  "band\_assoc"  0  THEN  Auto)\mcdot{})

---

Home Index