---

Step * of Lemma weak-antecedent-function-property

∀[es:EO]. ∀[P,Q:E ─→ ℙ]. ∀[f:{e:E| P e}  ─→ E].  f ∈ {e:E| P e}  ─→ {e:E| Q e}  supposing Q ←==f== P
BY
{ (Auto THEN Unfold `weak-antecedent-function` -1) }

1
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} 

---

Latex:


\mforall{}[es:EO].  \mforall{}[P,Q:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[f:\{e:E|  P  e\}    {}\mrightarrow{}  E].    f  \mmember{}  \{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\}    supposing  Q  \mleftarrow{}==f==  P


By

(Auto  THEN  Unfold  `weak-antecedent-function`  -1)

---

Home Index