---

Step * 2 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. ∃x:{x:ℝ| X x} . (↑(a x))
6. ∃x:{x:ℝ| X x} . (↑(b x))
7. ∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x)))
8. ∃x:ℝ. (((r0 < x) ∧ (x < r1)) ∧ (X x))
9. ∃x:ℝ. (((r1 < x) ∧ (x < r(2))) ∧ (X x))
⊢ ∃a0,b0:{x:ℝ| X x} . ((↑(a a0)) ∧ (↑(b b0)) ∧ a0 ≠ b0)
BY
{ ExRepD }

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
⊢ ∃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.  \mexists{}x:\{x:\mBbbR{}|  X  x\}  .  (\muparrow{}(a  x))
6.  \mexists{}x:\{x:\mBbbR{}|  X  x\}  .  (\muparrow{}(b  x))
7.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  ((\muparrow{}(a  x))  \mvee{}  (\muparrow{}(b  x)))
8.  \mexists{}x:\mBbbR{}.  (((r0  <  x)  \mwedge{}  (x  <  r1))  \mwedge{}  (X  x))
9.  \mexists{}x:\mBbbR{}.  (((r1  <  x)  \mwedge{}  (x  <  r(2)))  \mwedge{}  (X  x))
\mvdash{}  \mexists{}a0,b0:\{x:\mBbbR{}|  X  x\}  .  ((\muparrow{}(a  a0))  \mwedge{}  (\muparrow{}(b  b0))  \mwedge{}  a0  \mneq{}  b0)


By

---

Latex:
ExRepD

---

Home Index