---

Step * 1 of Lemma weak-antecedent-function-property


1. es : EO
2. P : E ─→ ℙ
3. Q : E ─→ ℙ
4. f : {e:E| P e}  ─→ E
5. ∀e:{e:E| P e} . (f e c≤ e ∧ (Q (f e)))
⊢ f ∈ {e:E| P e}  ─→ {e:E| Q e} 
BY
{ (ExtWith [`z'] [⌈{e:E| P e}  ─→ E⌉]⋅ THEN Auto) }

---

Latex:



1.  es  :  EO
2.  P  :  E  {}\mrightarrow{}  \mBbbP{}
3.  Q  :  E  {}\mrightarrow{}  \mBbbP{}
4.  f  :  \{e:E|  P  e\}    {}\mrightarrow{}  E
5.  \mforall{}e:\{e:E|  P  e\}  .  (f  e  c\mleq{}  e  \mwedge{}  (Q  (f  e)))
\mvdash{}  f  \mmember{}  \{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\} 


By

(ExtWith  [`z']  [\mkleeneopen{}\{e:E|  P  e\}    {}\mrightarrow{}  E\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index