---

Step * 1 3 of Lemma eo-restrict_property

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

1
1. es : EO@i'
2. P : E ─→ 𝔹@i
3. x : es-base-E(es)@i
4. ↑(es-dom(es) x)@i
5. ↑(P x)@i
⊢ x ∈ es-base-E(es)

2
.....set predicate..... 
1. es : EO@i'
2. P : E ─→ 𝔹@i
3. x : es-base-E(es)@i
4. ↑(es-dom(es) x)@i
5. ↑(P x)@i
⊢ ↑((es-dom(es) x) ∧b (P x))

3
.....wf..... 
1. es : EO@i'
2. P : E ─→ 𝔹@i
3. x : es-base-E(es)@i
4. ↑(es-dom(es) x)@i
5. ↑(P x)@i
6. e : es-base-E(es)
⊢ ↑((es-dom(es) e) ∧b (P e)) ∈ Type

---

Latex:


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


By

((D  -1  THEN  D  -2)  THEN  MemTypeCD)

---

Home Index