Step
*
1
of Lemma
real-subset-connected
.....assertion.....
1. X : ℝ ⟶ ℙ
2. ∀x:ℝ. SqStable(X x)
3. ∀x:ℝ. ∀y:{y:ℝ| x = y} . ((X y)
⇒ (X x))
4. dense-in-interval((-∞, ∞);X)
5. ∀Q:{x:ℝ| X x} ⟶ 𝔹. ∃Q':ℝ ⟶ 𝔹. ∀x:{x:ℝ| X x} . Q' x = Q x
⊢ ∀[A,B:{x:ℝ| X x} ⟶ ℙ].
((∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} . (A[y]
⇒ A[x]))
⇒ (∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} . (B[y]
⇒ B[x]))
⇒ (∀a,b:{x:ℝ| X x} ⟶ 𝔹.
((∀x:{x:ℝ| X x} . ((↑(a x))
⇒ A[x]))
⇒ (∀x:{x:ℝ| X x} . ((↑(b x))
⇒ B[x]))
⇒ (∃x:{x:ℝ| X x} . (↑(a x)))
⇒ (∃x:{x:ℝ| X x} . (↑(b x)))
⇒ (∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x))))
⇒ (∃r:{x:ℝ| X x} . (A[r] ∧ B[r])))))
BY
{ Auto }
1
1. X : ℝ ⟶ ℙ
2. ∀x:ℝ. SqStable(X x)
3. ∀x:ℝ. ∀y:{y:ℝ| x = y} . ((X y)
⇒ (X x))
4. dense-in-interval((-∞, ∞);X)
5. ∀Q:{x:ℝ| X x} ⟶ 𝔹. ∃Q':ℝ ⟶ 𝔹. ∀x:{x:ℝ| X x} . Q' x = Q x
6. [A] : {x:ℝ| X x} ⟶ ℙ
7. [B] : {x:ℝ| X x} ⟶ ℙ
8. ∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} . (A[y]
⇒ A[x])
9. ∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} . (B[y]
⇒ B[x])
10. a : {x:ℝ| X x} ⟶ 𝔹
11. b : {x:ℝ| X x} ⟶ 𝔹
12. ∀x:{x:ℝ| X x} . ((↑(a x))
⇒ A[x])
13. ∀x:{x:ℝ| X x} . ((↑(b x))
⇒ B[x])
14. ∃x:{x:ℝ| X x} . (↑(a x))
15. ∃x:{x:ℝ| X x} . (↑(b x))
16. ∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x)))
⊢ ∃r:{x:ℝ| X x} . (A[r] ∧ B[r])
Latex:
Latex:
.....assertion.....
1. X : \mBbbR{} {}\mrightarrow{} \mBbbP{}
2. \mforall{}x:\mBbbR{}. SqStable(X x)
3. \mforall{}x:\mBbbR{}. \mforall{}y:\{y:\mBbbR{}| x = y\} . ((X y) {}\mRightarrow{} (X x))
4. dense-in-interval((-\minfty{}, \minfty{});X)
5. \mforall{}Q:\{x:\mBbbR{}| X x\} {}\mrightarrow{} \mBbbB{}. \mexists{}Q':\mBbbR{} {}\mrightarrow{} \mBbbB{}. \mforall{}x:\{x:\mBbbR{}| X x\} . Q' x = Q x
\mvdash{} \mforall{}[A,B:\{x:\mBbbR{}| X x\} {}\mrightarrow{} \mBbbP{}].
((\mforall{}x:\{x:\mBbbR{}| X x\} . \mforall{}y:\{y:\{x:\mBbbR{}| X x\} | x = y\} . (A[y] {}\mRightarrow{} A[x]))
{}\mRightarrow{} (\mforall{}x:\{x:\mBbbR{}| X x\} . \mforall{}y:\{y:\{x:\mBbbR{}| X x\} | x = y\} . (B[y] {}\mRightarrow{} B[x]))
{}\mRightarrow{} (\mforall{}a,b:\{x:\mBbbR{}| X x\} {}\mrightarrow{} \mBbbB{}.
((\mforall{}x:\{x:\mBbbR{}| X x\} . ((\muparrow{}(a x)) {}\mRightarrow{} A[x]))
{}\mRightarrow{} (\mforall{}x:\{x:\mBbbR{}| X x\} . ((\muparrow{}(b x)) {}\mRightarrow{} B[x]))
{}\mRightarrow{} (\mexists{}x:\{x:\mBbbR{}| X x\} . (\muparrow{}(a x)))
{}\mRightarrow{} (\mexists{}x:\{x:\mBbbR{}| X x\} . (\muparrow{}(b x)))
{}\mRightarrow{} (\mforall{}x:\{x:\mBbbR{}| X x\} . ((\muparrow{}(a x)) \mvee{} (\muparrow{}(b x))))
{}\mRightarrow{} (\mexists{}r:\{x:\mBbbR{}| X x\} . (A[r] \mwedge{} B[r])))))
By
Latex:
Auto
Home
Index