---

Step * 2 1 1 1 1 1 2 2 of Lemma reals-connected


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. A[a]
7. b : ℝ
8. B[b]
9. d : r:ℝ ⟶ (A[r] ∨ B[r])
10. (∃x:ℝ. (↑isl(d x))) ⇒ (∃x:ℝ. (↑isr(d x))) ⇒ (∀x:ℝ. ((↑isl(d x)) ∨ (↑isr(d x)))) ⇒ (∃r:ℝ. (A[r] ∧ B[r]))
11. x : A[a]
12. (d a) = (inl x) ∈ (A[a] ∨ B[a])
13. y : B[b]
14. (d b) = (inr y ) ∈ (A[b] ∨ B[b])
15. x1 : ℝ
⊢ (↑isl(d x1)) ∨ (↑isr(d x1))
BY
{ ((GenConclTerm ⌜d x1⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
2.  [B]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:\mBbbR{}.  \mforall{}y:\{y:\mBbbR{}|  x  =  y\}  .    (A[y]  {}\mRightarrow{}  A[x])
4.  \mforall{}x:\mBbbR{}.  \mforall{}y:\{y:\mBbbR{}|  x  =  y\}  .    (B[y]  {}\mRightarrow{}  B[x])
5.  a  :  \mBbbR{}
6.  A[a]
7.  b  :  \mBbbR{}
8.  B[b]
9.  d  :  r:\mBbbR{}  {}\mrightarrow{}  (A[r]  \mvee{}  B[r])
10.  (\mexists{}x:\mBbbR{}.  (\muparrow{}isl(d  x)))
{}\mRightarrow{}  (\mexists{}x:\mBbbR{}.  (\muparrow{}isr(d  x)))
{}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  ((\muparrow{}isl(d  x))  \mvee{}  (\muparrow{}isr(d  x))))
{}\mRightarrow{}  (\mexists{}r:\mBbbR{}.  (A[r]  \mwedge{}  B[r]))
11.  x  :  A[a]
12.  (d  a)  =  (inl  x)
13.  y  :  B[b]
14.  (d  b)  =  (inr  y  )
15.  x1  :  \mBbbR{}
\mvdash{}  (\muparrow{}isl(d  x1))  \mvee{}  (\muparrow{}isr(d  x1))


By

---

Latex:
((GenConclTerm  \mkleeneopen{}d  x1\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Reduce  0  THEN  Auto)

---

Home Index