Theorem ovolval4

Description: The value of the Lebesgue outer measure for subsets of the reals. Similar to ovolval3 , but here f may represent unordered interval bounds. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovolval4.a	|- ( ph -> A C_ RR )
	ovolval4.m	|- M = { y e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) }
Assertion	ovolval4	|- ( ph -> ( vol* ` A ) = inf ( M , RR* , < ) )

Proof

Step	Hyp	Ref	Expression
1		ovolval4.a	|- ( ph -> A C_ RR )
2		ovolval4.m	|- M = { y e. RR* | E. f e. ( ( RR X. RR ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = ( sum^ ` ( ( vol o. (,) ) o. f ) ) ) }
3		2fveq3	|- ( k = n -> ( 1st ` ( f ` k ) ) = ( 1st ` ( f ` n ) ) )
4		2fveq3	|- ( k = n -> ( 2nd ` ( f ` k ) ) = ( 2nd ` ( f ` n ) ) )
5	3 4	breq12d	|- ( k = n -> ( ( 1st ` ( f ` k ) ) <_ ( 2nd ` ( f ` k ) ) <-> ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) ) )
6	5 4 3	ifbieq12d	|- ( k = n -> if ( ( 1st ` ( f ` k ) ) <_ ( 2nd ` ( f ` k ) ) , ( 2nd ` ( f ` k ) ) , ( 1st ` ( f ` k ) ) ) = if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) )
7	3 6	opeq12d	|- ( k = n -> <. ( 1st ` ( f ` k ) ) , if ( ( 1st ` ( f ` k ) ) <_ ( 2nd ` ( f ` k ) ) , ( 2nd ` ( f ` k ) ) , ( 1st ` ( f ` k ) ) ) >. = <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. )
8	7	cbvmptv	|- ( k e. NN |-> <. ( 1st ` ( f ` k ) ) , if ( ( 1st ` ( f ` k ) ) <_ ( 2nd ` ( f ` k ) ) , ( 2nd ` ( f ` k ) ) , ( 1st ` ( f ` k ) ) ) >. ) = ( n e. NN |-> <. ( 1st ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ ( 2nd ` ( f ` n ) ) , ( 2nd ` ( f ` n ) ) , ( 1st ` ( f ` n ) ) ) >. )
9	1 2 8	ovolval4lem2	|- ( ph -> ( vol* ` A ) = inf ( M , RR* , < ) )