---

Step * of Lemma real-subset-connected

∀X:ℝ ⟶ ℙ
  ((∀x:ℝ. SqStable(X x))
  ⇒ (∀x:ℝ. ∀y:{y:ℝ| x = y} .  ((X y) ⇒ (X x)))
  ⇒ dense-in-interval((-∞, ∞);X)
  ⇒ (∀Q:{x:ℝ| X x}  ⟶ 𝔹. ∃Q':ℝ ⟶ 𝔹. ∀x:{x:ℝ| X x} . Q' x = Q x)
  ⇒ Connected({x:ℝ| X x} ))
BY
{ (Auto
   THEN Assert ⌜∀[A,B:{x:ℝ| X x}  ⟶ ℙ].
                  ((∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (A[y] ⇒ A[x]))
                  ⇒ (∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (B[y] ⇒ B[x]))
                  ⇒ (∀a,b:{x:ℝ| X x}  ⟶ 𝔹.
                        ((∀x:{x:ℝ| X x} . ((↑(a x)) ⇒ A[x]))
                        ⇒ (∀x:{x:ℝ| X x} . ((↑(b x)) ⇒ B[x]))
                        ⇒ (∃x:{x:ℝ| X x} . (↑(a x)))
                        ⇒ (∃x:{x:ℝ| X x} . (↑(b x)))
                        ⇒ (∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x))))
                        ⇒ (∃r:{x:ℝ| X x} . (A[r] ∧ B[r])))))⌝⋅
   ) }

1
.....assertion..... 
1. X : ℝ ⟶ ℙ
2. ∀x:ℝ. SqStable(X x)
3. ∀x:ℝ. ∀y:{y:ℝ| x = y} .  ((X y) ⇒ (X x))
4. dense-in-interval((-∞, ∞);X)
5. ∀Q:{x:ℝ| X x}  ⟶ 𝔹. ∃Q':ℝ ⟶ 𝔹. ∀x:{x:ℝ| X x} . Q' x = Q x
⊢ ∀[A,B:{x:ℝ| X x}  ⟶ ℙ].
    ((∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (A[y] ⇒ A[x]))
    ⇒ (∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (B[y] ⇒ B[x]))
    ⇒ (∀a,b:{x:ℝ| X x}  ⟶ 𝔹.
          ((∀x:{x:ℝ| X x} . ((↑(a x)) ⇒ A[x]))
          ⇒ (∀x:{x:ℝ| X x} . ((↑(b x)) ⇒ B[x]))
          ⇒ (∃x:{x:ℝ| X x} . (↑(a x)))
          ⇒ (∃x:{x:ℝ| X x} . (↑(b x)))
          ⇒ (∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x))))
          ⇒ (∃r:{x:ℝ| X x} . (A[r] ∧ B[r])))))

2
1. X : ℝ ⟶ ℙ
2. ∀x:ℝ. SqStable(X x)
3. ∀x:ℝ. ∀y:{y:ℝ| x = y} .  ((X y) ⇒ (X x))
4. dense-in-interval((-∞, ∞);X)
5. ∀Q:{x:ℝ| X x}  ⟶ 𝔹. ∃Q':ℝ ⟶ 𝔹. ∀x:{x:ℝ| X x} . Q' x = Q x
6. ∀[A,B:{x:ℝ| X x}  ⟶ ℙ].
     ((∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (A[y] ⇒ A[x]))
     ⇒ (∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (B[y] ⇒ B[x]))
     ⇒ (∀a,b:{x:ℝ| X x}  ⟶ 𝔹.
           ((∀x:{x:ℝ| X x} . ((↑(a x)) ⇒ A[x]))
           ⇒ (∀x:{x:ℝ| X x} . ((↑(b x)) ⇒ B[x]))
           ⇒ (∃x:{x:ℝ| X x} . (↑(a x)))
           ⇒ (∃x:{x:ℝ| X x} . (↑(b x)))
           ⇒ (∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x))))
           ⇒ (∃r:{x:ℝ| X x} . (A[r] ∧ B[r])))))
⊢ Connected({x:ℝ| X x} )

---

Latex:

---

Latex:
\mforall{}X:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}
    ((\mforall{}x:\mBbbR{}.  SqStable(X  x))
    {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  \mforall{}y:\{y:\mBbbR{}|  x  =  y\}  .    ((X  y)  {}\mRightarrow{}  (X  x)))
    {}\mRightarrow{}  dense-in-interval((-\minfty{},  \minfty{});X)
    {}\mRightarrow{}  (\mforall{}Q:\{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  \mBbbB{}.  \mexists{}Q':\mBbbR{}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  Q'  x  =  Q  x)
    {}\mRightarrow{}  Connected(\{x:\mBbbR{}|  X  x\}  ))


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}\mforall{}[A,B:\{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  \mBbbP{}].
                                ((\mforall{}x:\{x:\mBbbR{}|  X  x\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  X  x\}  |  x  =  y\}  .    (A[y]  {}\mRightarrow{}  A[x]))
                                {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  X  x\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  X  x\}  |  x  =  y\}  .    (B[y]  {}\mRightarrow{}  B[x]))
                                {}\mRightarrow{}  (\mforall{}a,b:\{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  \mBbbB{}.
                                            ((\mforall{}x:\{x:\mBbbR{}|  X  x\}  .  ((\muparrow{}(a  x))  {}\mRightarrow{}  A[x]))
                                            {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  X  x\}  .  ((\muparrow{}(b  x))  {}\mRightarrow{}  B[x]))
                                            {}\mRightarrow{}  (\mexists{}x:\{x:\mBbbR{}|  X  x\}  .  (\muparrow{}(a  x)))
                                            {}\mRightarrow{}  (\mexists{}x:\{x:\mBbbR{}|  X  x\}  .  (\muparrow{}(b  x)))
                                            {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  X  x\}  .  ((\muparrow{}(a  x))  \mvee{}  (\muparrow{}(b  x))))
                                            {}\mRightarrow{}  (\mexists{}r:\{x:\mBbbR{}|  X  x\}  .  (A[r]  \mwedge{}  B[r])))))\mkleeneclose{}\mcdot{}
  )

---

Home Index