---

Step * 1 2 2 2 1 1 of Lemma weak-antecedent-conditional


1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [Q1] : E ─→ ℙ
4. [P2] : E ─→ ℙ
5. [Q2] : E ─→ ℙ
6. dcd_P1 : e:E ─→ Dec(P1 e)@i
7. f : {e:E| P1 e}  ─→ {e:E| Q1 e} @i
8. g : {e:E| P2 e}  ─→ {e:E| Q2 e} @i
9. ∀e:{e:E| P1 e} . (f e c≤ e ∧ (Q1 (f e)))@i
10. ∀e:{e:E| P2 e} . (g e c≤ e ∧ (Q2 (g e)))@i
11. e : {e:E| (P1 e) ∨ (P2 e)} @i
12. [P1? f : g] e c≤ e
13. ¬(P1 e)
14. y : ¬(P1 e)@i
15. (dcd_P1 e) = (inr y ) ∈ Dec(P1 e)@i
⊢ Q2 (g e)
BY
{ ((Assert e ∈ {e:E| P2 e}  BY (DVar `e' THEN SplitOrHyps THEN Auto)) THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  [P1]  :  E  {}\mrightarrow{}  \mBbbP{}
3.  [Q1]  :  E  {}\mrightarrow{}  \mBbbP{}
4.  [P2]  :  E  {}\mrightarrow{}  \mBbbP{}
5.  [Q2]  :  E  {}\mrightarrow{}  \mBbbP{}
6.  dcd$_{P1}$  :  e:E  {}\mrightarrow{}  Dec(P1  e)@i
7.  f  :  \{e:E|  P1  e\}    {}\mrightarrow{}  \{e:E|  Q1  e\}  @i
8.  g  :  \{e:E|  P2  e\}    {}\mrightarrow{}  \{e:E|  Q2  e\}  @i
9.  \mforall{}e:\{e:E|  P1  e\}  .  (f  e  c\mleq{}  e  \mwedge{}  (Q1  (f  e)))@i
10.  \mforall{}e:\{e:E|  P2  e\}  .  (g  e  c\mleq{}  e  \mwedge{}  (Q2  (g  e)))@i
11.  e  :  \{e:E|  (P1  e)  \mvee{}  (P2  e)\}  @i
12.  [P1?  f  :  g]  e  c\mleq{}  e
13.  \mneg{}(P1  e)
14.  y  :  \mneg{}(P1  e)@i
15.  (dcd$_{P1}$  e)  =  (inr  y  )@i
\mvdash{}  Q2  (g  e)


By

((Assert  e  \mmember{}  \{e:E|  P2  e\}    BY  (DVar  `e'  THEN  SplitOrHyps  THEN  Auto))  THEN  Auto)

---

Home Index