---

Step * 1 of Lemma existse-ge_wf


1. es : EO
2. e : E
3. P : {e':E| loc(e') = loc(e) ∈ Id}  ─→ ℙ
4. e' : E@i
5. e ≤loc e' 
⊢ e' ∈ {e':E| loc(e') = loc(e) ∈ Id} 
BY
{ (MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. es : EO
2. e : E
3. P : {e':E| loc(e') = loc(e) ∈ Id}  ─→ ℙ
4. e' : E@i
5. e ≤loc e' 
⊢ loc(e') = loc(e) ∈ Id

---

Latex:



1.  es  :  EO
2.  e  :  E
3.  P  :  \{e':E|  loc(e')  =  loc(e)\}    {}\mrightarrow{}  \mBbbP{}
4.  e'  :  E@i
5.  e  \mleq{}loc  e' 
\mvdash{}  e'  \mmember{}  \{e':E|  loc(e')  =  loc(e)\} 


By

(MemTypeCD  THEN  Auto)

---

Home Index