Step
*
1
1
1
4
2
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. e : {e:E| (P1 e) ∨ (P2 e)} @i
17. e' : {e:E| (P1 e) ∨ (P2 e)} @i
18. y : ¬(P1 e)
19. (dcd_P1 e) = (inr y ) ∈ Dec(P1 e)
20. y1 : ¬(P1 e')
21. (dcd_P1 e') = (inr y1 ) ∈ Dec(P1 e')
22. (Q1 ∨ Q2) (f2 e) (f2 e')
23. Q2 (f2 e) (f2 e')
⊢ R2 e e'
BY
{ Assert ⌈(e ∈ {e:E| P2 e} ) ∧ (e' ∈ {e:E| P2 e} )⌉⋅ }
1
.....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. y : ¬(P1 e)
19. (dcd_P1 e) = (inr y ) ∈ Dec(P1 e)
20. y1 : ¬(P1 e')
21. (dcd_P1 e') = (inr y1 ) ∈ Dec(P1 e')
22. (Q1 ∨ Q2) (f2 e) (f2 e')
23. Q2 (f2 e) (f2 e')
⊢ (e ∈ {e:E| P2 e} ) ∧ (e' ∈ {e:E| P2 e} )
2
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. y : ¬(P1 e)
19. (dcd_P1 e) = (inr y ) ∈ Dec(P1 e)
20. y1 : ¬(P1 e')
21. (dcd_P1 e') = (inr y1 ) ∈ Dec(P1 e')
22. (Q1 ∨ Q2) (f2 e) (f2 e')
23. Q2 (f2 e) (f2 e')
24. (e ∈ {e:E| P2 e} ) ∧ (e' ∈ {e:E| P2 e} )
⊢ 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. e : \{e:E| (P1 e) \mvee{} (P2 e)\} @i
17. e' : \{e:E| (P1 e) \mvee{} (P2 e)\} @i
18. y : \mneg{}(P1 e)
19. (dcd$_{P1}$ e) = (inr y )
20. y1 : \mneg{}(P1 e')
21. (dcd$_{P1}$ e') = (inr y1 )
22. (Q1 \mvee{} Q2) (f2 e) (f2 e')
23. Q2 (f2 e) (f2 e')
\mvdash{} R2 e e'
By
Assert \mkleeneopen{}(e \mmember{} \{e:E| P2 e\} ) \mwedge{} (e' \mmember{} \{e:E| P2 e\} )\mkleeneclose{}\mcdot{}
Home
Index