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

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 ⊢ 𝐽 = ( topGen ‘ ran (,) )
icccmp.2 ⊢ 𝑇 = ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) )
Assertion icccmp ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑇 ∈ Comp )

Proof

Step Hyp Ref Expression
1 icccmp.1 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 icccmp.2 ⊢ 𝑇 = ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) )
3 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
4 eqid ⊢ { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 } = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 }
5 simplll ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ( 𝑢 ∈ 𝒫 𝐽 ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 ) ) → 𝐴 ∈ ℝ )
6 simpllr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ( 𝑢 ∈ 𝒫 𝐽 ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 ) ) → 𝐵 ∈ ℝ )
7 simplr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ( 𝑢 ∈ 𝒫 𝐽 ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 ) ) → 𝐴 ≤ 𝐵 )
8 elpwi ⊢ ( 𝑢 ∈ 𝒫 𝐽 → 𝑢 ⊆ 𝐽 )
9 8 ad2antrl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ( 𝑢 ∈ 𝒫 𝐽 ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 ) ) → 𝑢 ⊆ 𝐽 )
10 simprr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ( 𝑢 ∈ 𝒫 𝐽 ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 )
11 1 2 3 4 5 6 7 9 10 icccmplem3 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ( 𝑢 ∈ 𝒫 𝐽 ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 ) ) → 𝐵 ∈ { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 } )
12 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 [,] 𝑥 ) = ( 𝐴 [,] 𝐵 ) )
13 12 sseq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 ↔ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑧 ) )
14 13 rexbidv ⊢ ( 𝑥 = 𝐵 → ( ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑧 ) )
15 14 elrab ⊢ ( 𝐵 ∈ { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 } ↔ ( 𝐵 ∈ ( 𝐴 [,] 𝐵 ) ∧ ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑧 ) )
16 15 simprbi ⊢ ( 𝐵 ∈ { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 } → ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑧 )
17 11 16 syl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ ( 𝑢 ∈ 𝒫 𝐽 ∧ ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑧 )
18 17 expr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) ∧ 𝑢 ∈ 𝒫 𝐽 ) → ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 → ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑧 ) )
19 18 ralrimiva ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ∀ 𝑢 ∈ 𝒫 𝐽 ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 → ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑧 ) )
20 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
21 1 20 eqeltri ⊢ 𝐽 ∈ Top
22 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
23 22 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
24 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
25 1 unieqi ⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) )
26 24 25 eqtr4i ⊢ ℝ = ∪ 𝐽
27 26 cmpsub ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) → ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Comp ↔ ∀ 𝑢 ∈ 𝒫 𝐽 ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 → ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑧 ) ) )
28 21 23 27 sylancr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Comp ↔ ∀ 𝑢 ∈ 𝒫 𝐽 ( ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑢 → ∃ 𝑧 ∈ ( 𝒫 𝑢 ∩ Fin ) ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑧 ) ) )
29 19 28 mpbird ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≤ 𝐵 ) → ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Comp )
30 rexr ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
31 rexr ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
32 icc0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
33 30 31 32 syl2an ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 [,] 𝐵 ) = ∅ ↔ 𝐵 < 𝐴 ) )
34 33 biimpar ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( 𝐴 [,] 𝐵 ) = ∅ )
35 34 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) = ( 𝐽 ↾t ∅ ) )
36 rest0 ⊢ ( 𝐽 ∈ Top → ( 𝐽 ↾t ∅ ) = { ∅ } )
37 21 36 ax-mp ⊢ ( 𝐽 ↾t ∅ ) = { ∅ }
38 35 37 eqtrdi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) = { ∅ } )
39 0cmp ⊢ { ∅ } ∈ Comp
40 38 39 eqeltrdi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐵 < 𝐴 ) → ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Comp )
41 lelttric ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴 ) )
42 29 40 41 mpjaodan ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) ) ∈ Comp )
43 2 42 eqeltrid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑇 ∈ Comp )