Metamath Proof Explorer

Theorem ivthlem1

Description: Lemma for ivth . The set S of all x values with ( Fx ) less than U is lower bounded by A and upper bounded by B . (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Hypotheses ivth.1 
|- ( ph -> A e. RR )
ivth.2 
|- ( ph -> B e. RR )
ivth.3 
|- ( ph -> U e. RR )
ivth.4 
|- ( ph -> A < B )
ivth.5 
|- ( ph -> ( A [,] B ) C_ D )
ivth.7 
|- ( ph -> F e. ( D -cn-> CC ) )
ivth.8 
|- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )
ivth.9 
|- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )
ivth.10 
|- S = { x e. ( A [,] B ) | ( F ` x ) <_ U }
Assertion ivthlem1 
|- ( ph -> ( A e. S /\ A. z e. S z <_ B ) )

Proof

Step Hyp Ref Expression
1 ivth.1 
 |-  ( ph -> A e. RR )
2 ivth.2 
 |-  ( ph -> B e. RR )
3 ivth.3 
 |-  ( ph -> U e. RR )
4 ivth.4 
 |-  ( ph -> A < B )
5 ivth.5 
 |-  ( ph -> ( A [,] B ) C_ D )
6 ivth.7 
 |-  ( ph -> F e. ( D -cn-> CC ) )
7 ivth.8 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )
8 ivth.9 
 |-  ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )
9 ivth.10 
 |-  S = { x e. ( A [,] B ) | ( F ` x ) <_ U }
10 1 rexrd 
 |-  ( ph -> A e. RR* )
11 2 rexrd 
 |-  ( ph -> B e. RR* )
12 1 2 4 ltled 
 |-  ( ph -> A <_ B )
13 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
14 10 11 12 13 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
15 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
16 15 eleq1d 
 |-  ( x = A -> ( ( F ` x ) e. RR <-> ( F ` A ) e. RR ) )
17 7 ralrimiva 
 |-  ( ph -> A. x e. ( A [,] B ) ( F ` x ) e. RR )
18 16 17 14 rspcdva 
 |-  ( ph -> ( F ` A ) e. RR )
19 8 simpld 
 |-  ( ph -> ( F ` A ) < U )
20 18 3 19 ltled 
 |-  ( ph -> ( F ` A ) <_ U )
21 15 breq1d 
 |-  ( x = A -> ( ( F ` x ) <_ U <-> ( F ` A ) <_ U ) )
22 21 9 elrab2 
 |-  ( A e. S <-> ( A e. ( A [,] B ) /\ ( F ` A ) <_ U ) )
23 14 20 22 sylanbrc 
 |-  ( ph -> A e. S )
24 9 ssrab3 
 |-  S C_ ( A [,] B )
25 24 sseli 
 |-  ( z e. S -> z e. ( A [,] B ) )
26 iccleub 
 |-  ( ( A e. RR* /\ B e. RR* /\ z e. ( A [,] B ) ) -> z <_ B )
27 26 3expia 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( z e. ( A [,] B ) -> z <_ B ) )
28 10 11 27 syl2anc 
 |-  ( ph -> ( z e. ( A [,] B ) -> z <_ B ) )
29 25 28 syl5 
 |-  ( ph -> ( z e. S -> z <_ B ) )
30 29 ralrimiv 
 |-  ( ph -> A. z e. S z <_ B )
31 23 30 jca 
 |-  ( ph -> ( A e. S /\ A. z e. S z <_ B ) )