---

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:

---

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

---

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

---

Home Index