---

Step * 1 of Lemma strong-subtype-eo-forward-E


1. eo : EO
2. e : {e:es-base-E(eo)| ↑(es-dom(eo) e)} 
3. eo.e ∈ EO
4. e1 : es-base-E(eo)@i
5. ↑(es-dom(eo.e) e1)@i
⊢ ↑(es-dom(eo) e1)
BY
{ RepUR ``es-dom eo-forward eo-restrict`` -1 }

1
1. eo : EO
2. e : {e:es-base-E(eo)| ↑(es-dom(eo) e)} 
3. eo.e ∈ EO
4. e1 : es-base-E(eo)@i
5. ↑((eo."dom" e1) ∧b (e ≤loc e1 ∨b(¬bloc(e1) = loc(e))))@i
⊢ ↑(es-dom(eo) e1)

---

Latex:



1.  eo  :  EO
2.  e  :  \{e:es-base-E(eo)|  \muparrow{}(es-dom(eo)  e)\} 
3.  eo.e  \mmember{}  EO
4.  e1  :  es-base-E(eo)@i
5.  \muparrow{}(es-dom(eo.e)  e1)@i
\mvdash{}  \muparrow{}(es-dom(eo)  e1)


By

RepUR  ``es-dom  eo-forward  eo-restrict``  -1

---

Home Index