Metamath Proof Explorer

Theorem iccioo01

Description: The closed unit interval is equinumerous to the open unit interval. Based on a Mastodon post by Michael Kinyon. (Contributed by Jim Kingdon, 4-Jun-2024)

Ref Expression
Assertion iccioo01 
|- ( 0 [,] 1 ) ~~ ( 0 (,) 1 )

Proof

Step Hyp Ref Expression
1 4nn 
 |-  4 e. NN
2 nnrecre 
 |-  ( 4 e. NN -> ( 1 / 4 ) e. RR )
3 1 2 ax-mp 
 |-  ( 1 / 4 ) e. RR
4 halfre 
 |-  ( 1 / 2 ) e. RR
5 2lt4 
 |-  2 < 4
6 2re 
 |-  2 e. RR
7 4re 
 |-  4 e. RR
8 2pos 
 |-  0 < 2
9 4pos 
 |-  0 < 4
10 6 7 8 9 ltrecii 
 |-  ( 2 < 4 <-> ( 1 / 4 ) < ( 1 / 2 ) )
11 5 10 mpbi 
 |-  ( 1 / 4 ) < ( 1 / 2 )
12 iccen 
 |-  ( ( ( 1 / 4 ) e. RR /\ ( 1 / 2 ) e. RR /\ ( 1 / 4 ) < ( 1 / 2 ) ) -> ( 0 [,] 1 ) ~~ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) )
13 3 4 11 12 mp3an 
 |-  ( 0 [,] 1 ) ~~ ( ( 1 / 4 ) [,] ( 1 / 2 ) )
14 ovex 
 |-  ( 0 (,) 1 ) e. _V
15 0xr 
 |-  0 e. RR*
16 1xr 
 |-  1 e. RR*
17 7 9 recgt0ii 
 |-  0 < ( 1 / 4 )
18 halflt1 
 |-  ( 1 / 2 ) < 1
19 iccssioo 
 |-  ( ( ( 0 e. RR* /\ 1 e. RR* ) /\ ( 0 < ( 1 / 4 ) /\ ( 1 / 2 ) < 1 ) ) -> ( ( 1 / 4 ) [,] ( 1 / 2 ) ) C_ ( 0 (,) 1 ) )
20 15 16 17 18 19 mp4an 
 |-  ( ( 1 / 4 ) [,] ( 1 / 2 ) ) C_ ( 0 (,) 1 )
21 ssdomg 
 |-  ( ( 0 (,) 1 ) e. _V -> ( ( ( 1 / 4 ) [,] ( 1 / 2 ) ) C_ ( 0 (,) 1 ) -> ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ~<_ ( 0 (,) 1 ) ) )
22 14 20 21 mp2 
 |-  ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ~<_ ( 0 (,) 1 )
23 endomtr 
 |-  ( ( ( 0 [,] 1 ) ~~ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) /\ ( ( 1 / 4 ) [,] ( 1 / 2 ) ) ~<_ ( 0 (,) 1 ) ) -> ( 0 [,] 1 ) ~<_ ( 0 (,) 1 ) )
24 13 22 23 mp2an 
 |-  ( 0 [,] 1 ) ~<_ ( 0 (,) 1 )
25 ovex 
 |-  ( 0 [,] 1 ) e. _V
26 ioossicc 
 |-  ( 0 (,) 1 ) C_ ( 0 [,] 1 )
27 ssdomg 
 |-  ( ( 0 [,] 1 ) e. _V -> ( ( 0 (,) 1 ) C_ ( 0 [,] 1 ) -> ( 0 (,) 1 ) ~<_ ( 0 [,] 1 ) ) )
28 25 26 27 mp2 
 |-  ( 0 (,) 1 ) ~<_ ( 0 [,] 1 )
29 sbth 
 |-  ( ( ( 0 [,] 1 ) ~<_ ( 0 (,) 1 ) /\ ( 0 (,) 1 ) ~<_ ( 0 [,] 1 ) ) -> ( 0 [,] 1 ) ~~ ( 0 (,) 1 ) )
30 24 28 29 mp2an 
 |-  ( 0 [,] 1 ) ~~ ( 0 (,) 1 )