---

Step * 1 1 1 1 of Lemma interval-connected


1. I : Interval
2. [A] : {x:ℝ| x ∈ I}  ⟶ ℙ
3. [B] : {x:ℝ| x ∈ I}  ⟶ ℙ
4. ∀x:{x:ℝ| x ∈ I} . ∀y:{y:{x:ℝ| x ∈ I} | x = y} .  (A[y] ⇒ A[x])
5. ∀x:{x:ℝ| x ∈ I} . ∀y:{y:{x:ℝ| x ∈ I} | x = y} .  (B[y] ⇒ B[x])
6. a : {x:ℝ| x ∈ I} 
7. A[a]
8. b : {x:ℝ| x ∈ I} 
9. B[b]
10. ∀r:{x:ℝ| x ∈ I} . (A[r] ∨ B[r])
11. [rmin(a;b), rmax(a;b)] ⊆ I 
12. (∀r:{x:ℝ| x ∈ [rmin(a;b), rmax(a;b)]} . (A[r] ∨ B[r])) ⇒ (∃r:{x:ℝ| x ∈ [rmin(a;b), rmax(a;b)]} . (A[r] ∧ B[r]))
⊢ ∃r:{x:ℝ| x ∈ I} . (A[r] ∧ B[r])
BY
{ (D -1 THENA Auto) }

1
1. I : Interval
2. [A] : {x:ℝ| x ∈ I}  ⟶ ℙ
3. [B] : {x:ℝ| x ∈ I}  ⟶ ℙ
4. ∀x:{x:ℝ| x ∈ I} . ∀y:{y:{x:ℝ| x ∈ I} | x = y} .  (A[y] ⇒ A[x])
5. ∀x:{x:ℝ| x ∈ I} . ∀y:{y:{x:ℝ| x ∈ I} | x = y} .  (B[y] ⇒ B[x])
6. a : {x:ℝ| x ∈ I} 
7. A[a]
8. b : {x:ℝ| x ∈ I} 
9. B[b]
10. ∀r:{x:ℝ| x ∈ I} . (A[r] ∨ B[r])
11. [rmin(a;b), rmax(a;b)] ⊆ I 
12. ∃r:{x:ℝ| x ∈ [rmin(a;b), rmax(a;b)]} . (A[r] ∧ B[r])
⊢ ∃r:{x:ℝ| x ∈ I} . (A[r] ∧ B[r])

---

Latex:

---

Latex:

1.  I  :  Interval
2.  [A]  :  \{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbP{}
3.  [B]  :  \{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  x  \mmember{}  I\}  |  x  =  y\}  .    (A[y]  {}\mRightarrow{}  A[x])
5.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  x  \mmember{}  I\}  |  x  =  y\}  .    (B[y]  {}\mRightarrow{}  B[x])
6.  a  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
7.  A[a]
8.  b  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
9.  B[b]
10.  \mforall{}r:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (A[r]  \mvee{}  B[r])
11.  [rmin(a;b),  rmax(a;b)]  \msubseteq{}  I 
12.  (\mforall{}r:\{x:\mBbbR{}|  x  \mmember{}  [rmin(a;b),  rmax(a;b)]\}  .  (A[r]  \mvee{}  B[r]))
{}\mRightarrow{}  (\mexists{}r:\{x:\mBbbR{}|  x  \mmember{}  [rmin(a;b),  rmax(a;b)]\}  .  (A[r]  \mwedge{}  B[r]))
\mvdash{}  \mexists{}r:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (A[r]  \mwedge{}  B[r])


By

---

Latex:
(D  -1  THENA  Auto)

---

Home Index