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	eqtrid	|- ( 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 )