---

Step * 2 of Lemma weak-antecedent-function_functionality_wrt_pred_equiv


1. es : EO@i'
2. [P] : E ─→ ℙ
3. [Q] : E ─→ ℙ
4. [P'] : E ─→ ℙ
5. [Q'] : E ─→ ℙ
6. f : {e:E| P e}  ─→ {e:E| Q e} @i
7. ∀x:E. (P x ⇐⇒ P' x)@i
8. ∀x:E. (Q x ⇐⇒ Q' x)@i
9. Q' ←==f== P'@i
⊢ Q ←==f== P
BY
{ All (RepUR ``weak-antecedent-function``)⋅ }

1
1. es : EO@i'
2. [P] : E ─→ ℙ
3. [Q] : E ─→ ℙ
4. [P'] : E ─→ ℙ
5. [Q'] : E ─→ ℙ
6. f : {e:E| P e}  ─→ {e:E| Q e} @i
7. ∀x:E. (P x ⇐⇒ P' x)@i
8. ∀x:E. (Q x ⇐⇒ Q' x)@i
9. ∀e:{e:E| P' e} . (f e c≤ e ∧ (Q' (f e)))@i
⊢ ∀e:{e:E| P e} . (f e c≤ e ∧ (Q (f e)))

---

Latex:



1.  es  :  EO@i'
2.  [P]  :  E  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  E  {}\mrightarrow{}  \mBbbP{}
4.  [P']  :  E  {}\mrightarrow{}  \mBbbP{}
5.  [Q']  :  E  {}\mrightarrow{}  \mBbbP{}
6.  f  :  \{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\}  @i
7.  \mforall{}x:E.  (P  x  \mLeftarrow{}{}\mRightarrow{}  P'  x)@i
8.  \mforall{}x:E.  (Q  x  \mLeftarrow{}{}\mRightarrow{}  Q'  x)@i
9.  Q'  \mleftarrow{}==f==  P'@i
\mvdash{}  Q  \mleftarrow{}==f==  P


By

All  (RepUR  ``weak-antecedent-function``)\mcdot{}

---

Home Index