Metamath Proof Explorer

Theorem ex-ovoliunnfl

Description: Demonstration of ovoliunnfl . (Contributed by Brendan Leahy, 21-Nov-2017)

Ref Expression
Assertion ex-ovoliunnfl 
|- ( ( A ~<_ NN /\ A. x e. A x ~<_ NN ) -> U. A =/= RR )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  seq 1 ( + , ( m e. NN |-> ( vol* ` ( f ` m ) ) ) ) = seq 1 ( + , ( m e. NN |-> ( vol* ` ( f ` m ) ) ) )
2 eqid 
 |-  ( m e. NN |-> ( vol* ` ( f ` m ) ) ) = ( m e. NN |-> ( vol* ` ( f ` m ) ) )
3 fveq2 
 |-  ( n = m -> ( f ` n ) = ( f ` m ) )
4 3 sseq1d 
 |-  ( n = m -> ( ( f ` n ) C_ RR <-> ( f ` m ) C_ RR ) )
5 2fveq3 
 |-  ( n = m -> ( vol* ` ( f ` n ) ) = ( vol* ` ( f ` m ) ) )
6 5 eleq1d 
 |-  ( n = m -> ( ( vol* ` ( f ` n ) ) e. RR <-> ( vol* ` ( f ` m ) ) e. RR ) )
7 4 6 anbi12d 
 |-  ( n = m -> ( ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) e. RR ) <-> ( ( f ` m ) C_ RR /\ ( vol* ` ( f ` m ) ) e. RR ) ) )
8 7 rspccva 
 |-  ( ( A. n e. NN ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) e. RR ) /\ m e. NN ) -> ( ( f ` m ) C_ RR /\ ( vol* ` ( f ` m ) ) e. RR ) )
9 8 simpld 
 |-  ( ( A. n e. NN ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) e. RR ) /\ m e. NN ) -> ( f ` m ) C_ RR )
10 9 adantll 
 |-  ( ( ( f Fn NN /\ A. n e. NN ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) e. RR ) ) /\ m e. NN ) -> ( f ` m ) C_ RR )
11 8 simprd 
 |-  ( ( A. n e. NN ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) e. RR ) /\ m e. NN ) -> ( vol* ` ( f ` m ) ) e. RR )
12 11 adantll 
 |-  ( ( ( f Fn NN /\ A. n e. NN ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) e. RR ) ) /\ m e. NN ) -> ( vol* ` ( f ` m ) ) e. RR )
13 1 2 10 12 ovoliun 
 |-  ( ( f Fn NN /\ A. n e. NN ( ( f ` n ) C_ RR /\ ( vol* ` ( f ` n ) ) e. RR ) ) -> ( vol* ` U_ m e. NN ( f ` m ) ) <_ sup ( ran seq 1 ( + , ( m e. NN |-> ( vol* ` ( f ` m ) ) ) ) , RR* , < ) )
14 13 ovoliunnfl 
 |-  ( ( A ~<_ NN /\ A. x e. A x ~<_ NN ) -> U. A =/= RR )