---

Step * 2 1 of Lemma real-subset-connected


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] : {x:ℝ| X x}  ⟶ ℙ
7. [B] : {x:ℝ| X x}  ⟶ ℙ
8. ∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (A[y] ⇒ A[x])
9. ∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (B[y] ⇒ B[x])
10. ∀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])))
11. a : {x:ℝ| X x} 
12. A[a]
13. b : {x:ℝ| X x} 
14. B[b]
15. d : r:{x:ℝ| X x}  ⟶ (A[r] ∨ B[r])
⊢ ∃r:{x:ℝ| X x} . (A[r] ∧ B[r])
BY
{ ((D -6 With ⌜λx.isl(d x)⌝  THENA Auto) THEN (D -1 With ⌜λx.isr(d x)⌝  THENA Auto) THEN Reduce -1) }

1
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] : {x:ℝ| X x}  ⟶ ℙ
7. [B] : {x:ℝ| X x}  ⟶ ℙ
8. ∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (A[y] ⇒ A[x])
9. ∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (B[y] ⇒ B[x])
10. a : {x:ℝ| X x} 
11. A[a]
12. b : {x:ℝ| X x} 
13. B[b]
14. d : r:{x:ℝ| X x}  ⟶ (A[r] ∨ B[r])
15. (∀x:{x:ℝ| X x} . ((↑isl(d x)) ⇒ A[x]))
⇒ (∀x:{x:ℝ| X x} . ((↑isr(d x)) ⇒ B[x]))
⇒ (∃x:{x:ℝ| X x} . (↑isl(d x)))
⇒ (∃x:{x:ℝ| X x} . (↑isr(d x)))
⇒ (∀x:{x:ℝ| X x} . ((↑isl(d x)) ∨ (↑isr(d x))))
⇒ (∃r:{x:ℝ| X x} . (A[r] ∧ B[r]))
⊢ ∃r:{x:ℝ| 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.  [A]  :  \{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  \mBbbP{}
7.  [B]  :  \{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  \mBbbP{}
8.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  X  x\}  |  x  =  y\}  .    (A[y]  {}\mRightarrow{}  A[x])
9.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  X  x\}  |  x  =  y\}  .    (B[y]  {}\mRightarrow{}  B[x])
10.  \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])))
11.  a  :  \{x:\mBbbR{}|  X  x\} 
12.  A[a]
13.  b  :  \{x:\mBbbR{}|  X  x\} 
14.  B[b]
15.  d  :  r:\{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  (A[r]  \mvee{}  B[r])
\mvdash{}  \mexists{}r:\{x:\mBbbR{}|  X  x\}  .  (A[r]  \mwedge{}  B[r])


By

---

Latex:
((D  -6  With  \mkleeneopen{}\mlambda{}x.isl(d  x)\mkleeneclose{}    THENA  Auto)  THEN  (D  -1  With  \mkleeneopen{}\mlambda{}x.isr(d  x)\mkleeneclose{}    THENA  Auto)  THEN  Reduce  -1)

---

Home Index