---

Step * 1 of Lemma antecedent-surjection_functionality_wrt_iff


1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [P2] : E ─→ ℙ
4. [Q1] : E ─→ ℙ
5. [Q2] : E ─→ ℙ
6. f : {e:E| P1 e}  ─→ {e:E| Q1 e} @i
7. ∀e:E. (P1 e ⇐⇒ P2 e)@i
8. ∀e:E. (Q1 e ⇐⇒ Q2 e)@i
9. ∀e:{e:E| Q1 e} . ∃e':{e:E| P1 e} . ((f e') = e ∈ E)@i
10. ∀e:{e:E| P1 e} . ((f e < e) ∧ (Q1 (f e)))@i
⊢ ∀e:{e:E| P2 e} . ((f e < e) ∧ (Q2 (f e)))
BY
{ (ParallelLast THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  [P1]  :  E  {}\mrightarrow{}  \mBbbP{}
3.  [P2]  :  E  {}\mrightarrow{}  \mBbbP{}
4.  [Q1]  :  E  {}\mrightarrow{}  \mBbbP{}
5.  [Q2]  :  E  {}\mrightarrow{}  \mBbbP{}
6.  f  :  \{e:E|  P1  e\}    {}\mrightarrow{}  \{e:E|  Q1  e\}  @i
7.  \mforall{}e:E.  (P1  e  \mLeftarrow{}{}\mRightarrow{}  P2  e)@i
8.  \mforall{}e:E.  (Q1  e  \mLeftarrow{}{}\mRightarrow{}  Q2  e)@i
9.  \mforall{}e:\{e:E|  Q1  e\}  .  \mexists{}e':\{e:E|  P1  e\}  .  ((f  e')  =  e)@i
10.  \mforall{}e:\{e:E|  P1  e\}  .  ((f  e  <  e)  \mwedge{}  (Q1  (f  e)))@i
\mvdash{}  \mforall{}e:\{e:E|  P2  e\}  .  ((f  e  <  e)  \mwedge{}  (Q2  (f  e)))


By

(ParallelLast  THEN  Auto)

---

Home Index