---

Step * 1 of Lemma closed-interval-connected


1. u : ℝ
2. v : ℝ
3. ∀[A,B:ℝ ⟶ ℙ].
     ((∀x:ℝ. ∀y:{y:ℝ| x = y} .  (A[y] ⇒ A[x]))
     ⇒ (∀x:ℝ. ∀y:{y:ℝ| x = y} .  (B[y] ⇒ B[x]))
     ⇒ (∃a:ℝ. A[a])
     ⇒ (∃b:ℝ. B[b])
     ⇒ (∀r:ℝ. (A[r] ∨ B[r]))
     ⇒ (∃r:ℝ. (A[r] ∧ B[r])))
4. [A] : {x:ℝ| x ∈ [u, v]}  ⟶ ℙ
5. [B] : {x:ℝ| x ∈ [u, v]}  ⟶ ℙ
6. ∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (A[y] ⇒ A[x])
7. ∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (B[y] ⇒ B[x])
8. a : {x:ℝ| x ∈ [u, v]} 
9. A[a]
10. b : {x:ℝ| x ∈ [u, v]} 
11. B[b]
12. ∀r:{x:ℝ| x ∈ [u, v]} . (A[r] ∨ B[r])
13. u ≤ v
⊢ ∃r:{x:ℝ| x ∈ [u, v]} . (A[r] ∧ B[r])
BY
{ ((D 3 With ⌜λx.A[interval-retraction(u;v;x)]⌝  THENA Auto)
   THEN (D -1 With ⌜λx.B[interval-retraction(u;v;x)]⌝  THENA Auto)
   THEN RepUR ``so_apply`` -1) }

1
1. u : ℝ
2. v : ℝ
3. [A] : {x:ℝ| x ∈ [u, v]}  ⟶ ℙ
4. [B] : {x:ℝ| x ∈ [u, v]}  ⟶ ℙ
5. ∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (A[y] ⇒ A[x])
6. ∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (B[y] ⇒ B[x])
7. a : {x:ℝ| x ∈ [u, v]} 
8. A[a]
9. b : {x:ℝ| x ∈ [u, v]} 
10. B[b]
11. ∀r:{x:ℝ| x ∈ [u, v]} . (A[r] ∨ B[r])
12. u ≤ v
13. (∀x:ℝ. ∀y:{y:ℝ| x = y} .  ((A interval-retraction(u;v;y)) ⇒ (A interval-retraction(u;v;x))))
⇒ (∀x:ℝ. ∀y:{y:ℝ| x = y} .  ((B interval-retraction(u;v;y)) ⇒ (B interval-retraction(u;v;x))))
⇒ (∃a:ℝ. (A interval-retraction(u;v;a)))
⇒ (∃b:ℝ. (B interval-retraction(u;v;b)))
⇒ (∀r:ℝ. ((A interval-retraction(u;v;r)) ∨ (B interval-retraction(u;v;r))))
⇒ (∃r:ℝ. ((A interval-retraction(u;v;r)) ∧ (B interval-retraction(u;v;r))))
⊢ ∃r:{x:ℝ| x ∈ [u, v]} . (A[r] ∧ B[r])

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}
3.  \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{}  (\mexists{}a:\mBbbR{}.  A[a])
          {}\mRightarrow{}  (\mexists{}b:\mBbbR{}.  B[b])
          {}\mRightarrow{}  (\mforall{}r:\mBbbR{}.  (A[r]  \mvee{}  B[r]))
          {}\mRightarrow{}  (\mexists{}r:\mBbbR{}.  (A[r]  \mwedge{}  B[r])))
4.  [A]  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}    {}\mrightarrow{}  \mBbbP{}
5.  [B]  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}    {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  |  x  =  y\}  .    (A[y]  {}\mRightarrow{}  A[x])
7.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  |  x  =  y\}  .    (B[y]  {}\mRightarrow{}  B[x])
8.  a  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\} 
9.  A[a]
10.  b  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\} 
11.  B[b]
12.  \mforall{}r:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .  (A[r]  \mvee{}  B[r])
13.  u  \mleq{}  v
\mvdash{}  \mexists{}r:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .  (A[r]  \mwedge{}  B[r])


By

---

Latex:
((D  3  With  \mkleeneopen{}\mlambda{}x.A[interval-retraction(u;v;x)]\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}\mlambda{}x.B[interval-retraction(u;v;x)]\mkleeneclose{}    THENA  Auto)
  THEN  RepUR  ``so\_apply``  -1)

---

Home Index