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* , < ) >. ) )