Metamath Proof Explorer

Theorem volsuplem

Description: Lemma for volsup . (Contributed by Mario Carneiro, 4-Jul-2014)

Ref Expression
Assertion volsuplem 
|- ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ ( A e. NN /\ B e. ( ZZ>= ` A ) ) ) -> ( F ` A ) C_ ( F ` B ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
2 1 sseq2d 
 |-  ( x = A -> ( ( F ` A ) C_ ( F ` x ) <-> ( F ` A ) C_ ( F ` A ) ) )
3 2 imbi2d 
 |-  ( x = A -> ( ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( F ` A ) C_ ( F ` x ) ) <-> ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( F ` A ) C_ ( F ` A ) ) ) )
4 fveq2 
 |-  ( x = k -> ( F ` x ) = ( F ` k ) )
5 4 sseq2d 
 |-  ( x = k -> ( ( F ` A ) C_ ( F ` x ) <-> ( F ` A ) C_ ( F ` k ) ) )
6 5 imbi2d 
 |-  ( x = k -> ( ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( F ` A ) C_ ( F ` x ) ) <-> ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( F ` A ) C_ ( F ` k ) ) ) )
7 fveq2 
 |-  ( x = ( k + 1 ) -> ( F ` x ) = ( F ` ( k + 1 ) ) )
8 7 sseq2d 
 |-  ( x = ( k + 1 ) -> ( ( F ` A ) C_ ( F ` x ) <-> ( F ` A ) C_ ( F ` ( k + 1 ) ) ) )
9 8 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( F ` A ) C_ ( F ` x ) ) <-> ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( F ` A ) C_ ( F ` ( k + 1 ) ) ) ) )
10 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
11 10 sseq2d 
 |-  ( x = B -> ( ( F ` A ) C_ ( F ` x ) <-> ( F ` A ) C_ ( F ` B ) ) )
12 11 imbi2d 
 |-  ( x = B -> ( ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( F ` A ) C_ ( F ` x ) ) <-> ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( F ` A ) C_ ( F ` B ) ) ) )
13 ssid 
 |-  ( F ` A ) C_ ( F ` A )
14 13 2a1i 
 |-  ( A e. ZZ -> ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( F ` A ) C_ ( F ` A ) ) )
15 eluznn 
 |-  ( ( A e. NN /\ k e. ( ZZ>= ` A ) ) -> k e. NN )
16 fveq2 
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
17 fvoveq1 
 |-  ( n = k -> ( F ` ( n + 1 ) ) = ( F ` ( k + 1 ) ) )
18 16 17 sseq12d 
 |-  ( n = k -> ( ( F ` n ) C_ ( F ` ( n + 1 ) ) <-> ( F ` k ) C_ ( F ` ( k + 1 ) ) ) )
19 18 rspccva 
 |-  ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ k e. NN ) -> ( F ` k ) C_ ( F ` ( k + 1 ) ) )
20 15 19 sylan2 
 |-  ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ ( A e. NN /\ k e. ( ZZ>= ` A ) ) ) -> ( F ` k ) C_ ( F ` ( k + 1 ) ) )
21 20 anassrs 
 |-  ( ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( F ` k ) C_ ( F ` ( k + 1 ) ) )
22 sstr2 
 |-  ( ( F ` A ) C_ ( F ` k ) -> ( ( F ` k ) C_ ( F ` ( k + 1 ) ) -> ( F ` A ) C_ ( F ` ( k + 1 ) ) ) )
23 21 22 syl5com 
 |-  ( ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) /\ k e. ( ZZ>= ` A ) ) -> ( ( F ` A ) C_ ( F ` k ) -> ( F ` A ) C_ ( F ` ( k + 1 ) ) ) )
24 23 expcom 
 |-  ( k e. ( ZZ>= ` A ) -> ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( ( F ` A ) C_ ( F ` k ) -> ( F ` A ) C_ ( F ` ( k + 1 ) ) ) ) )
25 24 a2d 
 |-  ( k e. ( ZZ>= ` A ) -> ( ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( F ` A ) C_ ( F ` k ) ) -> ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( F ` A ) C_ ( F ` ( k + 1 ) ) ) ) )
26 3 6 9 12 14 25 uzind4 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( F ` A ) C_ ( F ` B ) ) )
27 26 com12 
 |-  ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ A e. NN ) -> ( B e. ( ZZ>= ` A ) -> ( F ` A ) C_ ( F ` B ) ) )
28 27 impr 
 |-  ( ( A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) /\ ( A e. NN /\ B e. ( ZZ>= ` A ) ) ) -> ( F ` A ) C_ ( F ` B ) )