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

Metamath Proof Explorer

Theorem elovolm

Description: Elementhood in the set M of approximations to the outer measure. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypothesis elovolm.1 
|- M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
Assertion elovolm 
|- ( B e. M <-> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )

Proof

Step Hyp Ref Expression
1 elovolm.1 
 |-  M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
2 eqeq1 
 |-  ( y = B -> ( y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <-> B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
3 2 anbi2d 
 |-  ( y = B -> ( ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) <-> ( A C_ U. ran ( (,) o. f ) /\ B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) )
4 3 rexbidv 
 |-  ( y = B -> ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) <-> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) )
5 4 1 elrab2 
 |-  ( B e. M <-> ( B e. RR* /\ E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) )
6 elovolmlem 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> f : NN --> ( <_ i^i ( RR X. RR ) ) )
7 eqid 
 |-  ( ( abs o. - ) o. f ) = ( ( abs o. - ) o. f )
8 eqid 
 |-  seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) )
9 7 8 ovolsf 
 |-  ( f : NN --> ( <_ i^i ( RR X. RR ) ) -> seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) )
10 6 9 sylbi 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) )
11 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
12 fss 
 |-  ( ( seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR* ) -> seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> RR* )
13 10 11 12 sylancl 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> RR* )
14 frn 
 |-  ( seq 1 ( + , ( ( abs o. - ) o. f ) ) : NN --> RR* -> ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* )
15 supxrcl 
 |-  ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) C_ RR* -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* )
16 13 14 15 3syl 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* )
17 eleq1 
 |-  ( B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) -> ( B e. RR* <-> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) e. RR* ) )
18 16 17 syl5ibrcom 
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) -> ( B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) -> B e. RR* ) )
19 18 imp 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> B e. RR* )
20 19 adantrl 
 |-  ( ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( A C_ U. ran ( (,) o. f ) /\ B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) -> B e. RR* )
21 20 rexlimiva 
 |-  ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> B e. RR* )
22 21 pm4.71ri 
 |-  ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) <-> ( B e. RR* /\ E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) )
23 5 22 bitr4i 
 |-  ( B e. M <-> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ B = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )