---

Step * 1 of Lemma reals-connected

.....assertion..... 
∀[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])))))
BY
{ (Auto THEN (FLemma `inhabited-covers-real-implies-ext` [-1] THENA Auto) THEN RepeatFor 2 (Thin (-3)) 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 : ℝ ⟶ 𝔹
6. b : ℝ ⟶ 𝔹
7. ∀x:ℝ. ((↑(a x)) ⇒ A[x])
8. ∀x:ℝ. ((↑(b x)) ⇒ B[x])
9. ∀x:ℝ. ((↑(a x)) ∨ (↑(b x)))
10. f : ℕ ⟶ ℝ
11. g : ℕ ⟶ ℝ
12. x : ℝ
13. ∀n:ℕ. (↑(a (f n)))
14. ∀n:ℕ. (↑(b (g n)))
15. lim n→∞.f n = x
16. lim n→∞.g n = x
⊢ ∃r:ℝ. (A[r] ∧ B[r])

---

Latex:

---

Latex:
.....assertion..... 
\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])))))


By

---

Latex:
(Auto
  THEN  (FLemma  `inhabited-covers-real-implies-ext`  [-1]  THENA  Auto)
  THEN  RepeatFor  2  (Thin  (-3))
  THEN  ExRepD)

---

Home Index