This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iccen

Description: Any nontrivial closed interval is equinumerous to the unit interval. (Contributed by Mario Carneiro, 26-Jul-2014) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Assertion iccen 
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( 0 [,] 1 ) ~~ ( A [,] B ) )

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( 0 [,] 1 ) e. _V
2 ovex 
 |-  ( A [,] B ) e. _V
3 eqid 
 |-  ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) ) = ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )
4 3 iccf1o 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) ) : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) /\ `' ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) ) = ( y e. ( A [,] B ) |-> ( ( y - A ) / ( B - A ) ) ) ) )
5 4 simpld 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) ) : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) )
6 f1oen2g 
 |-  ( ( ( 0 [,] 1 ) e. _V /\ ( A [,] B ) e. _V /\ ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) ) : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) ) -> ( 0 [,] 1 ) ~~ ( A [,] B ) )
7 1 2 5 6 mp3an12i 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( 0 [,] 1 ) ~~ ( A [,] B ) )