---

Step * 1 of Lemma locl-pre-preserving-1-1


1. es : EO
2. P : E ─→ ℙ
3. f : {e:E| P e}  ─→ E
4. f is λe,e'. e ≤loc e' -λe,e'. e ≤loc e' -pre-preserving on P
⊢ Inj({e:E| P e} ;E;f)
BY
{ (Using [`Q',⌈λe,e'. e ≤loc e' ⌉;`R',⌈λe,e'. e ≤loc e' ⌉] (BLemma `Q-R-pre-preserving-1-1`)⋅ THEN Auto THEN Reduce 0) }

1
1. es : EO
2. P : E ─→ ℙ
3. f : {e:E| P e}  ─→ E
4. f is λe,e'. e ≤loc e' -λe,e'. e ≤loc e' -pre-preserving on P
⊢ Refl(E;e,e'.e ≤loc e' )

2
1. es : EO
2. P : E ─→ ℙ
3. f : {e:E| P e}  ─→ E
4. f is λe,e'. e ≤loc e' -λe,e'. e ≤loc e' -pre-preserving on P
⊢ AntiSym(E;e,e'.e ≤loc e' )

---

Latex:



1.  es  :  EO
2.  P  :  E  {}\mrightarrow{}  \mBbbP{}
3.  f  :  \{e:E|  P  e\}    {}\mrightarrow{}  E
4.  f  is  \mlambda{}e,e'.  e  \mleq{}loc  e'  -\mlambda{}e,e'.  e  \mleq{}loc  e'  -pre-preserving  on  P
\mvdash{}  Inj(\{e:E|  P  e\}  ;E;f)


By

(Using  [`Q',\mkleeneopen{}\mlambda{}e,e'.  e  \mleq{}loc  e'  \mkleeneclose{};`R',\mkleeneopen{}\mlambda{}e,e'.  e  \mleq{}loc  e'  \mkleeneclose{}]  (BLemma  `Q-R-pre-preserving-1-1`)\mcdot{}
  THEN  Auto
  THEN  Reduce  0)

---

Home Index