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

Metamath Proof Explorer

Theorem ioorval

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 = ( x e. ran (,) |-> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) )
Assertion ioorval 
|- ( A e. ran (,) -> ( F ` A ) = if ( A = (/) , <. 0 , 0 >. , <. inf ( A , RR* , < ) , sup ( A , RR* , < ) >. ) )

Proof

Step Hyp Ref Expression
1 ioorf.1 
 |-  F = ( x e. ran (,) |-> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) )
2 eqeq1 
 |-  ( x = A -> ( x = (/) <-> A = (/) ) )
3 infeq1 
 |-  ( x = A -> inf ( x , RR* , < ) = inf ( A , RR* , < ) )
4 supeq1 
 |-  ( x = A -> sup ( x , RR* , < ) = sup ( A , RR* , < ) )
5 3 4 opeq12d 
 |-  ( x = A -> <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. = <. inf ( A , RR* , < ) , sup ( A , RR* , < ) >. )
6 2 5 ifbieq2d 
 |-  ( x = A -> if ( x = (/) , <. 0 , 0 >. , <. inf ( x , RR* , < ) , sup ( x , RR* , < ) >. ) = if ( A = (/) , <. 0 , 0 >. , <. inf ( A , RR* , < ) , sup ( A , RR* , < ) >. ) )
7 opex 
 |-  <. 0 , 0 >. e. _V
8 opex 
 |-  <. inf ( A , RR* , < ) , sup ( A , RR* , < ) >. e. _V
9 7 8 ifex 
 |-  if ( A = (/) , <. 0 , 0 >. , <. inf ( A , RR* , < ) , sup ( A , RR* , < ) >. ) e. _V
10 6 1 9 fvmpt 
 |-  ( A e. ran (,) -> ( F ` A ) = if ( A = (/) , <. 0 , 0 >. , <. inf ( A , RR* , < ) , sup ( A , RR* , < ) >. ) )