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 )