---

Step * 1 of Lemma eo-restrict_property


1. es : EO@i'
2. P : E ⟶ 𝔹@i
⊢ {e:es."E"| ↑((es."dom" e) ∧b (P e))}  ≡ {e:E| ↑(P e)} 
BY
{ (RepUR ``es-E`` 0 THEN Folds ``es-base-E es-dom`` 0 THEN D 0 THEN D 0) }

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

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

3
.....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))} 

4
.....eq aux..... 
1. es : EO@i'
2. P : E ⟶ 𝔹@i
⊢ {e:{e:es-base-E(es)| ↑(es-dom(es) e)} | ↑(P e)}  ∈ Type

---

Latex:

---

Latex:

1.  es  :  EO@i'
2.  P  :  E  {}\mrightarrow{}  \mBbbB{}@i
\mvdash{}  \{e:es."E"|  \muparrow{}((es."dom"  e)  \mwedge{}\msubb{}  (P  e))\}    \mequiv{}  \{e:E|  \muparrow{}(P  e)\} 


By

---

Latex:
(RepUR  ``es-E``  0  THEN  Folds  ``es-base-E  es-dom``  0  THEN  D  0  THEN  D  0)

---

Home Index