---

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

.....wf..... 
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. y : ¬(P1 e)@i
13. (dcd_P1 e) = (inr y ) ∈ Dec(P1 e)@i
⊢ e ∈ {e:E| P2 e} 
BY
{ ((D (-3) THEN MemTypeCD THEN Auto) THEN ProveProp) }

---

Latex:


.....wf..... 
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.  y  :  \mneg{}(P1  e)@i
13.  (dcd$_{P1}$  e)  =  (inr  y  )@i
\mvdash{}  e  \mmember{}  \{e:E|  P2  e\} 


By

((D  (-3)  THEN  MemTypeCD  THEN  Auto)  THEN  ProveProp)

---

Home Index