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 )