---

Step * of Lemma reals-connected

Connected(ℝ)
BY
{ Assert ⌜∀[A,B:ℝ ⟶ ℙ].
            ((∀x:ℝ. ∀y:{y:ℝ| x = y} .  (A[y] ⇒ A[x]))
            ⇒ (∀x:ℝ. ∀y:{y:ℝ| x = y} .  (B[y] ⇒ B[x]))
            ⇒ (∀a,b:ℝ ⟶ 𝔹.
                  ((∀x:ℝ. ((↑(a x)) ⇒ A[x]))
                  ⇒ (∀x:ℝ. ((↑(b x)) ⇒ B[x]))
                  ⇒ (∃x:ℝ. (↑(a x)))
                  ⇒ (∃x:ℝ. (↑(b x)))
                  ⇒ (∀x:ℝ. ((↑(a x)) ∨ (↑(b x))))
                  ⇒ (∃r:ℝ. (A[r] ∧ B[r])))))⌝⋅ }

1
.....assertion..... 
∀[A,B:ℝ ⟶ ℙ].
  ((∀x:ℝ. ∀y:{y:ℝ| x = y} .  (A[y] ⇒ A[x]))
  ⇒ (∀x:ℝ. ∀y:{y:ℝ| x = y} .  (B[y] ⇒ B[x]))
  ⇒ (∀a,b:ℝ ⟶ 𝔹.
        ((∀x:ℝ. ((↑(a x)) ⇒ A[x]))
        ⇒ (∀x:ℝ. ((↑(b x)) ⇒ B[x]))
        ⇒ (∃x:ℝ. (↑(a x)))
        ⇒ (∃x:ℝ. (↑(b x)))
        ⇒ (∀x:ℝ. ((↑(a x)) ∨ (↑(b x))))
        ⇒ (∃r:ℝ. (A[r] ∧ B[r])))))

2
1. ∀[A,B:ℝ ⟶ ℙ].
     ((∀x:ℝ. ∀y:{y:ℝ| x = y} .  (A[y] ⇒ A[x]))
     ⇒ (∀x:ℝ. ∀y:{y:ℝ| x = y} .  (B[y] ⇒ B[x]))
     ⇒ (∀a,b:ℝ ⟶ 𝔹.
           ((∀x:ℝ. ((↑(a x)) ⇒ A[x]))
           ⇒ (∀x:ℝ. ((↑(b x)) ⇒ B[x]))
           ⇒ (∃x:ℝ. (↑(a x)))
           ⇒ (∃x:ℝ. (↑(b x)))
           ⇒ (∀x:ℝ. ((↑(a x)) ∨ (↑(b x))))
           ⇒ (∃r:ℝ. (A[r] ∧ B[r])))))
⊢ Connected(ℝ)

---

Latex:

---

Latex:
Connected(\mBbbR{})


By

---

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

---

Home Index