---

Step * 1 1 of Lemma range_sup_functionality


1. I : {I:Interval| icompact(I)} 
2. f : {x:ℝ| x ∈ I}  ⟶ ℝ
3. ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f[x] = f[y]))
4. ∀g:{x:ℝ| x ∈ I}  ⟶ ℝ
     (sup{f[x] | x ∈ I} = sup{g[x] | x ∈ I}) supposing 
        (((∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[x] = g[y])) ∧ (∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[y] = g[x]))) and\000C 
        (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))))
5. g : {x:ℝ| x ∈ I}  ⟶ ℝ
6. (sup{f[x] | x ∈ I} = sup{g[x] | x ∈ I}) supposing 
      (((∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[x] = g[y])) ∧ (∀x:{x:ℝ| x ∈ I} . ∃y:{x:ℝ| x ∈ I} . (f[y] = g[x]))) and 
      (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (g[x] = g[y]))))
7. ∀x:{x:ℝ| x ∈ I} . (f[x] = g[x])
8. x : {x:ℝ| x ∈ I} 
9. ∀y:{x:ℝ| x ∈ I} . ((x = y) ⇒ (f[x] = f[y]))
10. y : {x:ℝ| x ∈ I} 
11. x = y
12. f[x] = f[y]
⊢ g[x] = g[y]
BY
{ (RWO "-6" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  \{I:Interval|  icompact(I)\} 
2.  f  :  \{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbR{}
3.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))
4.  \mforall{}g:\{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbR{}
          (sup\{f[x]  |  x  \mmember{}  I\}  =  sup\{g[x]  |  x  \mmember{}  I\})  supposing 
                (((\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mexists{}y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f[x]  =  g[y]))
                \mwedge{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mexists{}y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f[y]  =  g[x])))  and 
                (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y]))))
5.  g  :  \{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbR{}
6.  (sup\{f[x]  |  x  \mmember{}  I\}  =  sup\{g[x]  |  x  \mmember{}  I\})  supposing 
            (((\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mexists{}y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f[x]  =  g[y]))
            \mwedge{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mexists{}y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f[y]  =  g[x])))  and 
            (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y]))))
7.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (f[x]  =  g[x])
8.  x  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
9.  \mforall{}y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))
10.  y  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
11.  x  =  y
12.  f[x]  =  f[y]
\mvdash{}  g[x]  =  g[y]


By

---

Latex:
(RWO  "-6"  (-1)  THEN  Auto)

---

Home Index