---

Step * 1 1 1 of Lemma eo-restrict_property


1. es : EO@i'
2. P : E ─→ 𝔹@i
3. x : es-base-E(es)@i
4. ↑((es-dom(es) x) ∧b (P x))@i
⊢ x ∈ {e:es-base-E(es)| ↑(es-dom(es) e)} 
BY
{ (MemTypeCD THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  P  :  E  {}\mrightarrow{}  \mBbbB{}@i
3.  x  :  es-base-E(es)@i
4.  \muparrow{}((es-dom(es)  x)  \mwedge{}\msubb{}  (P  x))@i
\mvdash{}  x  \mmember{}  \{e:es-base-E(es)|  \muparrow{}(es-dom(es)  e)\} 


By

(MemTypeCD  THEN  Auto)

---

Home Index