---

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

.....assertion..... 
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
⊢ Dec(P1 e)
BY
{ (With ⌈e⌉ (D 6)⋅ THEN Auto) }

---

Latex:


.....assertion..... 
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
\mvdash{}  Dec(P1  e)


By

(With  \mkleeneopen{}e\mkleeneclose{}  (D  6)\mcdot{}  THEN  Auto)

---

Home Index