---

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


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. [P1? f1 : f2] ∈ {t:E| P1[t] ∨ P2[t]}  ─→ E
17. e : {e:E| (λx.((P1 x) ∨ (P2 x))) e} @i
18. e' : {e:E| (P1 e) ∨ (P2 e)} @i
19. (Q1 ∨ Q2) ([P1? f1 : f2] e) ([P1? f1 : f2] e')@i
⊢ (R1 ∨ R2) e e'
BY
{ Thin (-4) }

1
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| (λx.((P1 x) ∨ (P2 x))) e} @i
17. e' : {e:E| (P1 e) ∨ (P2 e)} @i
18. (Q1 ∨ Q2) ([P1? f1 : f2] e) ([P1? f1 : f2] e')@i
⊢ (R1 ∨ R2) e e'

---

Latex:



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.  [P1?  f1  :  f2]  \mmember{}  \{t:E|  P1[t]  \mvee{}  P2[t]\}    {}\mrightarrow{}  E
17.  e  :  \{e:E|  (\mlambda{}x.((P1  x)  \mvee{}  (P2  x)))  e\}  @i
18.  e'  :  \{e:E|  (P1  e)  \mvee{}  (P2  e)\}  @i
19.  (Q1  \mvee{}  Q2)  ([P1?  f1  :  f2]  e)  ([P1?  f1  :  f2]  e')@i
\mvdash{}  (R1  \mvee{}  R2)  e  e'


By

Thin  (-4)

---

Home Index