Metamath Proof Explorer

Theorem icccmp

Description: A closed interval in RR is compact. (Contributed by Mario Carneiro, 13-Jun-2014)

Ref Expression
Hypotheses icccmp.1 
|- J = ( topGen ` ran (,) )
icccmp.2 
|- T = ( J |`t ( A [,] B ) )
Assertion icccmp 
|- ( ( A e. RR /\ B e. RR ) -> T e. Comp )

Proof

Step Hyp Ref Expression
1 icccmp.1 
 |-  J = ( topGen ` ran (,) )
2 icccmp.2 
 |-  T = ( J |`t ( A [,] B ) )
3 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
4 eqid 
 |-  { x e. ( A [,] B ) | E. z e. ( ~P u i^i Fin ) ( A [,] x ) C_ U. z } = { x e. ( A [,] B ) | E. z e. ( ~P u i^i Fin ) ( A [,] x ) C_ U. z }
5 simplll 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> A e. RR )
6 simpllr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> B e. RR )
7 simplr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> A <_ B )
8 elpwi 
 |-  ( u e. ~P J -> u C_ J )
9 8 ad2antrl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> u C_ J )
10 simprr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> ( A [,] B ) C_ U. u )
11 1 2 3 4 5 6 7 9 10 icccmplem3 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> B e. { x e. ( A [,] B ) | E. z e. ( ~P u i^i Fin ) ( A [,] x ) C_ U. z } )
12 oveq2 
 |-  ( x = B -> ( A [,] x ) = ( A [,] B ) )
13 12 sseq1d 
 |-  ( x = B -> ( ( A [,] x ) C_ U. z <-> ( A [,] B ) C_ U. z ) )
14 13 rexbidv 
 |-  ( x = B -> ( E. z e. ( ~P u i^i Fin ) ( A [,] x ) C_ U. z <-> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) )
15 14 elrab 
 |-  ( B e. { x e. ( A [,] B ) | E. z e. ( ~P u i^i Fin ) ( A [,] x ) C_ U. z } <-> ( B e. ( A [,] B ) /\ E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) )
16 15 simprbi 
 |-  ( B e. { x e. ( A [,] B ) | E. z e. ( ~P u i^i Fin ) ( A [,] x ) C_ U. z } -> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z )
17 11 16 syl 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ ( u e. ~P J /\ ( A [,] B ) C_ U. u ) ) -> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z )
18 17 expr 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) /\ u e. ~P J ) -> ( ( A [,] B ) C_ U. u -> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) )
19 18 ralrimiva 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> A. u e. ~P J ( ( A [,] B ) C_ U. u -> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) )
20 retop 
 |-  ( topGen ` ran (,) ) e. Top
21 1 20 eqeltri 
 |-  J e. Top
22 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
23 22 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( A [,] B ) C_ RR )
24 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
25 1 unieqi 
 |-  U. J = U. ( topGen ` ran (,) )
26 24 25 eqtr4i 
 |-  RR = U. J
27 26 cmpsub 
 |-  ( ( J e. Top /\ ( A [,] B ) C_ RR ) -> ( ( J |`t ( A [,] B ) ) e. Comp <-> A. u e. ~P J ( ( A [,] B ) C_ U. u -> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) ) )
28 21 23 27 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( ( J |`t ( A [,] B ) ) e. Comp <-> A. u e. ~P J ( ( A [,] B ) C_ U. u -> E. z e. ( ~P u i^i Fin ) ( A [,] B ) C_ U. z ) ) )
29 19 28 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ A <_ B ) -> ( J |`t ( A [,] B ) ) e. Comp )
30 rexr 
 |-  ( A e. RR -> A e. RR* )
31 rexr 
 |-  ( B e. RR -> B e. RR* )
32 icc0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> B < A ) )
33 30 31 32 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A [,] B ) = (/) <-> B < A ) )
34 33 biimpar 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( A [,] B ) = (/) )
35 34 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( J |`t ( A [,] B ) ) = ( J |`t (/) ) )
36 rest0 
 |-  ( J e. Top -> ( J |`t (/) ) = { (/) } )
37 21 36 ax-mp 
 |-  ( J |`t (/) ) = { (/) }
38 35 37 eqtrdi 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( J |`t ( A [,] B ) ) = { (/) } )
39 0cmp 
 |-  { (/) } e. Comp
40 38 39 eqeltrdi 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ B < A ) -> ( J |`t ( A [,] B ) ) e. Comp )
41 lelttric 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B \/ B < A ) )
42 29 40 41 mpjaodan 
 |-  ( ( A e. RR /\ B e. RR ) -> ( J |`t ( A [,] B ) ) e. Comp )
43 2 42 eqeltrid 
 |-  ( ( A e. RR /\ B e. RR ) -> T e. Comp )