This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ivth

Description: The intermediate value theorem, increasing case. This is Metamath 100 proof #79. (Contributed by Paul Chapman, 22-Jan-2008) (Proof shortened by Mario Carneiro, 30-Apr-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 ) ) )
Assertion ivth 
|- ( ph -> E. c e. ( A (,) B ) ( F ` c ) = U )

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 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
10 9 breq1d 
 |-  ( y = x -> ( ( F ` y ) <_ U <-> ( F ` x ) <_ U ) )
11 10 cbvrabv 
 |-  { y e. ( A [,] B ) | ( F ` y ) <_ U } = { x e. ( A [,] B ) | ( F ` x ) <_ U }
12 eqid 
 |-  sup ( { y e. ( A [,] B ) | ( F ` y ) <_ U } , RR , < ) = sup ( { y e. ( A [,] B ) | ( F ` y ) <_ U } , RR , < )
13 1 2 3 4 5 6 7 8 11 12 ivthlem3 
 |-  ( ph -> ( sup ( { y e. ( A [,] B ) | ( F ` y ) <_ U } , RR , < ) e. ( A (,) B ) /\ ( F ` sup ( { y e. ( A [,] B ) | ( F ` y ) <_ U } , RR , < ) ) = U ) )
14 fveqeq2 
 |-  ( c = sup ( { y e. ( A [,] B ) | ( F ` y ) <_ U } , RR , < ) -> ( ( F ` c ) = U <-> ( F ` sup ( { y e. ( A [,] B ) | ( F ` y ) <_ U } , RR , < ) ) = U ) )
15 14 rspcev 
 |-  ( ( sup ( { y e. ( A [,] B ) | ( F ` y ) <_ U } , RR , < ) e. ( A (,) B ) /\ ( F ` sup ( { y e. ( A [,] B ) | ( F ` y ) <_ U } , RR , < ) ) = U ) -> E. c e. ( A (,) B ) ( F ` c ) = U )
16 13 15 syl 
 |-  ( ph -> E. c e. ( A (,) B ) ( F ` c ) = U )