Step
*
of Lemma
weak-antecedent-surjection-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 D -1) THEN FLemma `weak-antecedent-function-property` [-2] THEN Auto) }
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{}\mleftarrow{}= f== \000CP
By
((Auto THEN D -1) THEN FLemma `weak-antecedent-function-property` [-2] THEN Auto)
Home
Index