---

Step * 2 of Lemma reals-connected


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(ℝ)
BY
{ (Unfold `connected` 0
   THEN (RepeatFor 4 ((ParallelLast'  THENA Auto)) THEN Auto)
   THEN RenameVar `d' (-1)
   THEN RepUR ``all of`` -1
   THEN ExRepD) }

1
1. [A] : ℝ ⟶ ℙ
2. [B] : ℝ ⟶ ℙ
3. ∀x:ℝ. ∀y:{y:ℝ| x = y} .  (A[y] ⇒ A[x])
4. ∀x:ℝ. ∀y:{y:ℝ| x = y} .  (B[y] ⇒ B[x])
5. ∀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])))
6. a : ℝ
7. A[a]
8. b : ℝ
9. B[b]
10. d : r:ℝ ⟶ (A[r] ∨ B[r])
⊢ ∃r:ℝ. (A[r] ∧ B[r])

---

Latex:

---

Latex:

1.  \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])))))
\mvdash{}  Connected(\mBbbR{})


By

---

Latex:
(Unfold  `connected`  0
  THEN  (RepeatFor  4  ((ParallelLast'    THENA  Auto))  THEN  Auto)
  THEN  RenameVar  `d'  (-1)
  THEN  RepUR  ``all  of``  -1
  THEN  ExRepD)

---

Home Index