---

Step * 1 2 2 of Lemma no-real-separation


1. A : ℝ ⟶ ℙ
2. B : ℝ ⟶ ℙ
3. real-disjoint(x.A[x];y.B[y])
4. x : ℝ
5. A[x]
6. y : ℝ
7. B[y]
8. d : r:ℝ ⟶ (A[r] + B[r])
9. ¬(∃x,y:ℝ. ((x = y) ∧ (↑isl(d x)) ∧ (↑isr(d y))))
10. ∀x,y:ℝ.  isl(d x) = isl(d y)
⊢ False
BY
{ ((InstHyp [⌜x⌝;⌜y⌝] (-1)⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜d x⌝;⌜d y⌝]⋅
   THEN (D -4 THEN Reduce 0)
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

1
1. A : ℝ ⟶ ℙ
2. B : ℝ ⟶ ℙ
3. real-disjoint(x.A[x];y.B[y])
4. x : ℝ
5. A[x]
6. y : ℝ
7. B[y]
8. d : r:ℝ ⟶ (A[r] + B[r])
9. ¬(∃x,y:ℝ. ((x = y) ∧ (↑isl(d x)) ∧ (↑isr(d y))))
10. ∀x,y:ℝ.  isl(d x) = isl(d y)
11. x1 : A[x]
12. (d x) = (inl x1) ∈ (A[x] + B[x])
13. x2 : A[y]
14. (d y) = (inl x2) ∈ (A[y] + B[y])
15. tt = tt
⊢ False

2
1. A : ℝ ⟶ ℙ
2. B : ℝ ⟶ ℙ
3. real-disjoint(x.A[x];y.B[y])
4. x : ℝ
5. A[x]
6. y : ℝ
7. B[y]
8. d : r:ℝ ⟶ (A[r] + B[r])
9. ¬(∃x,y:ℝ. ((x = y) ∧ (↑isl(d x)) ∧ (↑isr(d y))))
10. ∀x,y:ℝ.  isl(d x) = isl(d y)
11. y1 : B[x]
12. (d x) = (inr y1 ) ∈ (A[x] + B[x])
13. y2 : B[y]
14. (d y) = (inr y2 ) ∈ (A[y] + B[y])
15. ff = ff
⊢ False

---

Latex:

---

Latex:

1.  A  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
2.  B  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
3.  real-disjoint(x.A[x];y.B[y])
4.  x  :  \mBbbR{}
5.  A[x]
6.  y  :  \mBbbR{}
7.  B[y]
8.  d  :  r:\mBbbR{}  {}\mrightarrow{}  (A[r]  +  B[r])
9.  \mneg{}(\mexists{}x,y:\mBbbR{}.  ((x  =  y)  \mwedge{}  (\muparrow{}isl(d  x))  \mwedge{}  (\muparrow{}isr(d  y))))
10.  \mforall{}x,y:\mBbbR{}.    isl(d  x)  =  isl(d  y)
\mvdash{}  False


By

---

Latex:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}d  x\mkleeneclose{};\mkleeneopen{}d  y\mkleeneclose{}]\mcdot{}
  THEN  (D  -4  THEN  Reduce  0)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index