Metamath Proof Explorer


Theorem ioorf

Description: Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by AV, 13-Sep-2020)

Ref Expression
Hypothesis ioorf.1 F=xran.ifx=00supx*<supx*<
Assertion ioorf F:ran.*×*

Proof

Step Hyp Ref Expression
1 ioorf.1 F=xran.ifx=00supx*<supx*<
2 ioof .:*×*𝒫
3 ffn .:*×*𝒫.Fn*×*
4 ovelrn .Fn*×*xran.a*b*x=ab
5 2 3 4 mp2b xran.a*b*x=ab
6 0le0 00
7 df-br 0000
8 6 7 mpbi 00
9 0xr 0*
10 opelxpi 0*0*00*×*
11 9 9 10 mp2an 00*×*
12 8 11 elini 00*×*
13 12 a1i a*b*x=abx=00*×*
14 simplr a*b*x=ab¬x=x=ab
15 14 infeq1d a*b*x=ab¬x=supx*<=supab*<
16 simplll a*b*x=ab¬x=a*
17 simpllr a*b*x=ab¬x=b*
18 simpr a*b*x=ab¬x=¬x=
19 18 neqned a*b*x=ab¬x=x
20 14 19 eqnetrrd a*b*x=ab¬x=ab
21 df-ioo .=x*,y*z*|x<zz<y
22 idd w*b*w<bw<b
23 xrltle w*b*w<bwb
24 idd a*w*a<wa<w
25 xrltle a*w*a<waw
26 21 22 23 24 25 ixxlb a*b*absupab*<=a
27 16 17 20 26 syl3anc a*b*x=ab¬x=supab*<=a
28 15 27 eqtrd a*b*x=ab¬x=supx*<=a
29 14 supeq1d a*b*x=ab¬x=supx*<=supab*<
30 21 22 23 24 25 ixxub a*b*absupab*<=b
31 16 17 20 30 syl3anc a*b*x=ab¬x=supab*<=b
32 29 31 eqtrd a*b*x=ab¬x=supx*<=b
33 28 32 opeq12d a*b*x=ab¬x=supx*<supx*<=ab
34 ioon0 a*b*aba<b
35 34 ad2antrr a*b*x=ab¬x=aba<b
36 20 35 mpbid a*b*x=ab¬x=a<b
37 xrltle a*b*a<bab
38 37 ad2antrr a*b*x=ab¬x=a<bab
39 36 38 mpd a*b*x=ab¬x=ab
40 df-br abab
41 39 40 sylib a*b*x=ab¬x=ab
42 opelxpi a*b*ab*×*
43 42 ad2antrr a*b*x=ab¬x=ab*×*
44 41 43 elind a*b*x=ab¬x=ab*×*
45 33 44 eqeltrd a*b*x=ab¬x=supx*<supx*<*×*
46 13 45 ifclda a*b*x=abifx=00supx*<supx*<*×*
47 46 ex a*b*x=abifx=00supx*<supx*<*×*
48 47 rexlimivv a*b*x=abifx=00supx*<supx*<*×*
49 5 48 sylbi xran.ifx=00supx*<supx*<*×*
50 1 49 fmpti F:ran.*×*