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 𝑡 A B
Assertion icccmp A B T Comp

Proof

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