---

Step * 1 1 1 1 1 of Lemma Q-R-pre-preserving-conditional

.....assertion..... 
1. es : EO@i'
2. [P1] : E ─→ ℙ
3. [P2] : E ─→ ℙ
4. [Q1] : E ─→ E ─→ ℙ
5. [R1] : E ─→ E ─→ ℙ
6. [Q2] : E ─→ E ─→ ℙ
7. [R2] : E ─→ E ─→ ℙ
8. dcd_P1 : e:E ─→ Dec(P1 e)@i
9. f1 : {e:E| P1 e}  ─→ E@i
10. f2 : {e:E| P2 e}  ─→ E@i
11. ∀e,e':{e:E| P1 e} .  (¬(Q2 (f1 e) (f1 e')))
12. ∀e,e':{e:E| P2 e} .  (¬(Q1 (f2 e) (f2 e')))
13. ∀e:{e:E| P1 e} . ∀e':{e:E| P2 e} .
      ((¬(Q1 (f1 e) (f2 e'))) ∧ (¬(Q1 (f2 e') (f1 e))) ∧ (¬(Q2 (f1 e) (f2 e'))) ∧ (¬(Q2 (f2 e') (f1 e))))
14. ∀e,e':{e:E| P1 e} .  ((Q1 (f1 e) (f1 e')) ⇒ (R1 e e'))@i
15. ∀e,e':{e:E| P2 e} .  ((Q2 (f2 e) (f2 e')) ⇒ (R2 e e'))@i
16. e : {e:E| (P1 e) ∨ (P2 e)} @i
17. e' : {e:E| (P1 e) ∨ (P2 e)} @i
18. x : P1 e
19. (dcd_P1 e) = (inl x) ∈ Dec(P1 e)
20. x1 : P1 e'
21. (dcd_P1 e') = (inl x1) ∈ Dec(P1 e')
22. (Q1 ∨ Q2) (f1 e) (f1 e')
⊢ Q1 (f1 e) (f1 e')
BY
{ (RepUR ``rel_or infix_ap`` (-1)
   THEN (D -1 THEN Auto)
   THEN OnMaybeHyp 11 (\h. (InstHyp [⌈e⌉;⌈e'⌉] h⋅ THEN Auto THEN ProveProp THEN Auto)))⋅ }

---

Latex:


.....assertion..... 
1.  es  :  EO@i'
2.  [P1]  :  E  {}\mrightarrow{}  \mBbbP{}
3.  [P2]  :  E  {}\mrightarrow{}  \mBbbP{}
4.  [Q1]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
5.  [R1]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
6.  [Q2]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
7.  [R2]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
8.  dcd$_{P1}$  :  e:E  {}\mrightarrow{}  Dec(P1  e)@i
9.  f1  :  \{e:E|  P1  e\}    {}\mrightarrow{}  E@i
10.  f2  :  \{e:E|  P2  e\}    {}\mrightarrow{}  E@i
11.  \mforall{}e,e':\{e:E|  P1  e\}  .    (\mneg{}(Q2  (f1  e)  (f1  e')))
12.  \mforall{}e,e':\{e:E|  P2  e\}  .    (\mneg{}(Q1  (f2  e)  (f2  e')))
13.  \mforall{}e:\{e:E|  P1  e\}  .  \mforall{}e':\{e:E|  P2  e\}  .
            ((\mneg{}(Q1  (f1  e)  (f2  e')))
            \mwedge{}  (\mneg{}(Q1  (f2  e')  (f1  e)))
            \mwedge{}  (\mneg{}(Q2  (f1  e)  (f2  e')))
            \mwedge{}  (\mneg{}(Q2  (f2  e')  (f1  e))))
14.  \mforall{}e,e':\{e:E|  P1  e\}  .    ((Q1  (f1  e)  (f1  e'))  {}\mRightarrow{}  (R1  e  e'))@i
15.  \mforall{}e,e':\{e:E|  P2  e\}  .    ((Q2  (f2  e)  (f2  e'))  {}\mRightarrow{}  (R2  e  e'))@i
16.  e  :  \{e:E|  (P1  e)  \mvee{}  (P2  e)\}  @i
17.  e'  :  \{e:E|  (P1  e)  \mvee{}  (P2  e)\}  @i
18.  x  :  P1  e
19.  (dcd$_{P1}$  e)  =  (inl  x)
20.  x1  :  P1  e'
21.  (dcd$_{P1}$  e')  =  (inl  x1)
22.  (Q1  \mvee{}  Q2)  (f1  e)  (f1  e')
\mvdash{}  Q1  (f1  e)  (f1  e')


By

(RepUR  ``rel\_or  infix\_ap``  (-1)
  THEN  (D  -1  THEN  Auto)
  THEN  OnMaybeHyp  11  (\mbackslash{}h.  (InstHyp  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]  h\mcdot{}  THEN  Auto  THEN  ProveProp  THEN  Auto)))\mcdot{}

---

Home Index