Step
*
1
of Lemma
es-interval-iseg
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j)
⇒ (∀e2,e1:E. (e1 ≤loc e2
⇒ e1 ≤loc k
⇒ ([e1, e2] ≤ [e1, k]
⇐⇒ e2 ≤loc k ))))@i
5. e2 : E@i
6. e1 : E@i
7. e1 ≤loc e2 @i
8. e1 ≤loc j @i
⊢ [e1, e2] ≤ [e1, j]
⇐⇒ e2 ≤loc j
BY
{ (((RWO "es-le-iff" (-1)) THENA Auto) THEN (D (-1)) THEN ExRepD) }
1
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j)
⇒ (∀e2,e1:E. (e1 ≤loc e2
⇒ e1 ≤loc k
⇒ ([e1, e2] ≤ [e1, k]
⇐⇒ e2 ≤loc k ))))@i
5. e2 : E@i
6. e1 : E@i
7. e1 ≤loc e2 @i
8. ¬↑first(j)
9. e1 ≤loc pred(j)
⊢ [e1, e2] ≤ [e1, j]
⇐⇒ e2 ≤loc j
2
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j)
⇒ (∀e2,e1:E. (e1 ≤loc e2
⇒ e1 ≤loc k
⇒ ([e1, e2] ≤ [e1, k]
⇐⇒ e2 ≤loc k ))))@i
5. e2 : E@i
6. e1 : E@i
7. e1 ≤loc e2 @i
8. e1 = j ∈ E
⊢ [e1, e2] ≤ [e1, j]
⇐⇒ e2 ≤loc j
Latex:
1. es : EO@i'
2. WellFnd\{i\}(E;x,y.(x <loc y))
3. j : E@i
4. \mforall{}k:E
((k <loc j)
{}\mRightarrow{} (\mforall{}e2,e1:E. (e1 \mleq{}loc e2 {}\mRightarrow{} e1 \mleq{}loc k {}\mRightarrow{} ([e1, e2] \mleq{} [e1, k] \mLeftarrow{}{}\mRightarrow{} e2 \mleq{}loc k ))))@i
5. e2 : E@i
6. e1 : E@i
7. e1 \mleq{}loc e2 @i
8. e1 \mleq{}loc j @i
\mvdash{} [e1, e2] \mleq{} [e1, j] \mLeftarrow{}{}\mRightarrow{} e2 \mleq{}loc j
By
(((RWO "es-le-iff" (-1)) THENA Auto) THEN (D (-1)) THEN ExRepD)
Home
Index