Step * 2 of Lemma real-subset-connected


1. : ℝ ⟶ ℙ
2. ∀x:ℝSqStable(X x)
3. ∀x:ℝ. ∀y:{y:ℝy} .  ((X y)  (X x))
4. dense-in-interval((-∞, ∞);X)
5. ∀Q:{x:ℝx}  ⟶ 𝔹. ∃Q':ℝ ⟶ 𝔹. ∀x:{x:ℝx} Q' x
6. ∀[A,B:{x:ℝx}  ⟶ ℙ].
     ((∀x:{x:ℝx} . ∀y:{y:{x:ℝx} y} .  (A[y]  A[x]))
      (∀x:{x:ℝx} . ∀y:{y:{x:ℝx} y} .  (B[y]  B[x]))
      (∀a,b:{x:ℝx}  ⟶ 𝔹.
           ((∀x:{x:ℝx} ((↑(a x))  A[x]))
            (∀x:{x:ℝx} ((↑(b x))  B[x]))
            (∃x:{x:ℝx} (↑(a x)))
            (∃x:{x:ℝx} (↑(b x)))
            (∀x:{x:ℝx} ((↑(a x)) ∨ (↑(b x))))
            (∃r:{x:ℝx} (A[r] ∧ B[r])))))
⊢ Connected({x:ℝx} )
BY
(Unfold `connected` 0
   THEN (RepeatFor ((ParallelLast'  THENA Auto)) THEN Auto)
   THEN RenameVar `d' (-1)
   THEN RepUR ``all of`` -1
   THEN ExRepD) }

1
1. : ℝ ⟶ ℙ
2. ∀x:ℝSqStable(X x)
3. ∀x:ℝ. ∀y:{y:ℝy} .  ((X y)  (X x))
4. dense-in-interval((-∞, ∞);X)
5. ∀Q:{x:ℝx}  ⟶ 𝔹. ∃Q':ℝ ⟶ 𝔹. ∀x:{x:ℝx} Q' x
6. [A] {x:ℝx}  ⟶ ℙ
7. [B] {x:ℝx}  ⟶ ℙ
8. ∀x:{x:ℝx} . ∀y:{y:{x:ℝx} y} .  (A[y]  A[x])
9. ∀x:{x:ℝx} . ∀y:{y:{x:ℝx} y} .  (B[y]  B[x])
10. ∀a,b:{x:ℝx}  ⟶ 𝔹.
      ((∀x:{x:ℝx} ((↑(a x))  A[x]))
       (∀x:{x:ℝx} ((↑(b x))  B[x]))
       (∃x:{x:ℝx} (↑(a x)))
       (∃x:{x:ℝx} (↑(b x)))
       (∀x:{x:ℝx} ((↑(a x)) ∨ (↑(b x))))
       (∃r:{x:ℝx} (A[r] ∧ B[r])))
11. {x:ℝx} 
12. A[a]
13. {x:ℝx} 
14. B[b]
15. r:{x:ℝx}  ⟶ (A[r] ∨ B[r])
⊢ ∃r:{x:ℝx} (A[r] ∧ B[r])


Latex:


Latex:

1.  X  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}x:\mBbbR{}.  SqStable(X  x)
3.  \mforall{}x:\mBbbR{}.  \mforall{}y:\{y:\mBbbR{}|  x  =  y\}  .    ((X  y)  {}\mRightarrow{}  (X  x))
4.  dense-in-interval((-\minfty{},  \minfty{});X)
5.  \mforall{}Q:\{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  \mBbbB{}.  \mexists{}Q':\mBbbR{}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  Q'  x  =  Q  x
6.  \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])))))
\mvdash{}  Connected(\{x:\mBbbR{}|  X  x\}  )


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