---

Step * 2 1 1 1 of Lemma real-subset-connected-lemma


1. X : ℝ ⟶ ℙ
2. ∀a,b:{r:ℝ| r ∈ (-∞, ∞)} .  ((a < b) ⇒ (∃x:ℝ. (((a < x) ∧ (x < b)) ∧ (X x))))
3. a : {x:ℝ| X x}  ⟶ 𝔹
4. b : {x:ℝ| X x}  ⟶ 𝔹
5. x3 : {x:ℝ| X x} 
6. ↑(a x3)
7. x2 : {x:ℝ| X x} 
8. ↑(b x2)
9. ∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x)))
10. x1 : ℝ
11. r0 < x1
12. x1 < r1
13. X x1
14. x : ℝ
15. r1 < x
16. x < r(2)
17. X x
⊢ ∃a0,b0:{x:ℝ| X x} . ((↑(a a0)) ∧ (↑(b b0)) ∧ a0 ≠ b0)
BY
{ (InstLemma `rless-cases` [⌜x1⌝;⌜x⌝;⌜x3⌝]⋅ THENA Auto) }

1
1. X : ℝ ⟶ ℙ
2. ∀a,b:{r:ℝ| r ∈ (-∞, ∞)} .  ((a < b) ⇒ (∃x:ℝ. (((a < x) ∧ (x < b)) ∧ (X x))))
3. a : {x:ℝ| X x}  ⟶ 𝔹
4. b : {x:ℝ| X x}  ⟶ 𝔹
5. x3 : {x:ℝ| X x} 
6. ↑(a x3)
7. x2 : {x:ℝ| X x} 
8. ↑(b x2)
9. ∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x)))
10. x1 : ℝ
11. r0 < x1
12. x1 < r1
13. X x1
14. x : ℝ
15. r1 < x
16. x < r(2)
17. X x
18. (x1 < x3) ∨ (x3 < x)
⊢ ∃a0,b0:{x:ℝ| X x} . ((↑(a a0)) ∧ (↑(b b0)) ∧ a0 ≠ b0)

---

Latex:

---

Latex:

1.  X  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}a,b:\{r:\mBbbR{}|  r  \mmember{}  (-\minfty{},  \minfty{})\}  .    ((a  <  b)  {}\mRightarrow{}  (\mexists{}x:\mBbbR{}.  (((a  <  x)  \mwedge{}  (x  <  b))  \mwedge{}  (X  x))))
3.  a  :  \{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  \mBbbB{}
4.  b  :  \{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  \mBbbB{}
5.  x3  :  \{x:\mBbbR{}|  X  x\} 
6.  \muparrow{}(a  x3)
7.  x2  :  \{x:\mBbbR{}|  X  x\} 
8.  \muparrow{}(b  x2)
9.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  ((\muparrow{}(a  x))  \mvee{}  (\muparrow{}(b  x)))
10.  x1  :  \mBbbR{}
11.  r0  <  x1
12.  x1  <  r1
13.  X  x1
14.  x  :  \mBbbR{}
15.  r1  <  x
16.  x  <  r(2)
17.  X  x
\mvdash{}  \mexists{}a0,b0:\{x:\mBbbR{}|  X  x\}  .  ((\muparrow{}(a  a0))  \mwedge{}  (\muparrow{}(b  b0))  \mwedge{}  a0  \mneq{}  b0)


By

---

Latex:
(InstLemma  `rless-cases`  [\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x3\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index