Step
*
2
1
1
1
1
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]))
⊢ ∃r:ℝ. (A[r] ∧ B[r])
BY
{ ((GenConclTerm ⌜d a⌝⋅ THENA Auto) THEN D -2) }
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. 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])
⊢ ∃r:ℝ. (A[r] ∧ B[r])
2
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. y : B[a]
12. (d a) = (inr y ) ∈ (A[a] ∨ B[a])
⊢ ∃r:ℝ. (A[r] ∧ B[r])
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]))
\mvdash{} \mexists{}r:\mBbbR{}. (A[r] \mwedge{} B[r])
By
Latex:
((GenConclTerm \mkleeneopen{}d a\mkleeneclose{}\mcdot{} THENA Auto) THEN D -2)
Home
Index