Metamath Proof Explorer

Theorem elovolmr

Description: Sufficient condition for elementhood in the set M . (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Hypotheses 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* , < ) ) }
elovolmr.2 
|- S = seq 1 ( + , ( ( abs o. - ) o. F ) )
Assertion elovolmr 
|- ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> sup ( ran S , RR* , < ) e. M )

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 elovolmr.2 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. F ) )
3 elovolmlem 
 |-  ( F e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> F : NN --> ( <_ i^i ( RR X. RR ) ) )
4 id 
 |-  ( f = F -> f = F )
5 4 eqcomd 
 |-  ( f = F -> F = f )
6 5 coeq2d 
 |-  ( f = F -> ( ( abs o. - ) o. F ) = ( ( abs o. - ) o. f ) )
7 6 seqeq3d 
 |-  ( f = F -> seq 1 ( + , ( ( abs o. - ) o. F ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) ) )
8 2 7 syl5eq 
 |-  ( f = F -> S = seq 1 ( + , ( ( abs o. - ) o. f ) ) )
9 8 rneqd 
 |-  ( f = F -> ran S = ran seq 1 ( + , ( ( abs o. - ) o. f ) ) )
10 9 supeq1d 
 |-  ( f = F -> sup ( ran S , RR* , < ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) )
11 10 biantrud 
 |-  ( f = F -> ( A C_ U. ran ( (,) o. f ) <-> ( A C_ U. ran ( (,) o. f ) /\ sup ( ran S , RR* , < ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) )
12 coeq2 
 |-  ( f = F -> ( (,) o. f ) = ( (,) o. F ) )
13 12 rneqd 
 |-  ( f = F -> ran ( (,) o. f ) = ran ( (,) o. F ) )
14 13 unieqd 
 |-  ( f = F -> U. ran ( (,) o. f ) = U. ran ( (,) o. F ) )
15 14 sseq2d 
 |-  ( f = F -> ( A C_ U. ran ( (,) o. f ) <-> A C_ U. ran ( (,) o. F ) ) )
16 11 15 bitr3d 
 |-  ( f = F -> ( ( A C_ U. ran ( (,) o. f ) /\ sup ( ran S , RR* , < ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) <-> A C_ U. ran ( (,) o. F ) ) )
17 16 rspcev 
 |-  ( ( F e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ A C_ U. ran ( (,) o. F ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ sup ( ran S , RR* , < ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
18 3 17 sylanbr 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ sup ( ran S , RR* , < ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
19 1 elovolm 
 |-  ( sup ( ran S , RR* , < ) e. M <-> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ sup ( ran S , RR* , < ) = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) )
20 18 19 sylibr 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ A C_ U. ran ( (,) o. F ) ) -> sup ( ran S , RR* , < ) e. M )