---

Step * 1 2 of Lemma eo-restrict_property

.....eq aux..... 
1. es : EO@i'
2. P : E ─→ 𝔹@i
⊢ {e:es-base-E(es)| ↑((es-dom(es) e) ∧b (P e))}  ∈ Type
BY
{ MemCD }

1
.....subterm..... T:t
1:n
1. es : EO@i'
2. P : E ─→ 𝔹@i
⊢ es-base-E(es) ∈ Type

2
.....subterm..... T:t
2:n
1. es : EO@i'
2. P : E ─→ 𝔹@i
3. e : es-base-E(es)
⊢ ↑((es-dom(es) e) ∧b (P e)) ∈ Type

---

Latex:


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


By

MemCD

---

Home Index