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 \in ℝ \land B \in ℝ) \to T \in Comp$

Proof

Step	Hyp	Ref	Expression
1		icccmp.1	$⊢ J = topGen (ran (.))$
2		icccmp.2	$⊢ T = J ↾_{𝑡} [A, B]$
3		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
4		eqid	$⊢ \{x \in [A, B] \| \exists z \in (𝒫 u \cap Fin) [A, x] \subseteq ⋃ z\} = \{x \in [A, B] \| \exists z \in (𝒫 u \cap Fin) [A, x] \subseteq ⋃ z\}$
5		simplll	$⊢ (((A \in ℝ \land B \in ℝ) \land A \leq B) \land (u \in 𝒫 J \land [A, B] \subseteq ⋃ u)) \to A \in ℝ$
6		simpllr	$⊢ (((A \in ℝ \land B \in ℝ) \land A \leq B) \land (u \in 𝒫 J \land [A, B] \subseteq ⋃ u)) \to B \in ℝ$
7		simplr	$⊢ (((A \in ℝ \land B \in ℝ) \land A \leq B) \land (u \in 𝒫 J \land [A, B] \subseteq ⋃ u)) \to A \leq B$
8		elpwi	$⊢ u \in 𝒫 J \to u \subseteq J$
9	8	ad2antrl	$⊢ (((A \in ℝ \land B \in ℝ) \land A \leq B) \land (u \in 𝒫 J \land [A, B] \subseteq ⋃ u)) \to u \subseteq J$
10		simprr	$⊢ (((A \in ℝ \land B \in ℝ) \land A \leq B) \land (u \in 𝒫 J \land [A, B] \subseteq ⋃ u)) \to [A, B] \subseteq ⋃ u$
11	1 2 3 4 5 6 7 9 10	icccmplem3	$⊢ (((A \in ℝ \land B \in ℝ) \land A \leq B) \land (u \in 𝒫 J \land [A, B] \subseteq ⋃ u)) \to B \in \{x \in [A, B] \| \exists z \in (𝒫 u \cap Fin) [A, x] \subseteq ⋃ z\}$
12		oveq2	$⊢ x = B \to [A, x] = [A, B]$
13	12	sseq1d	$⊢ x = B \to ([A, x] \subseteq ⋃ z \leftrightarrow [A, B] \subseteq ⋃ z)$
14	13	rexbidv	$⊢ x = B \to (\exists z \in (𝒫 u \cap Fin) [A, x] \subseteq ⋃ z \leftrightarrow \exists z \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ z)$
15	14	elrab	$⊢ B \in \{x \in [A, B] \| \exists z \in (𝒫 u \cap Fin) [A, x] \subseteq ⋃ z\} \leftrightarrow (B \in [A, B] \land \exists z \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ z)$
16	15	simprbi	$⊢ B \in \{x \in [A, B] \| \exists z \in (𝒫 u \cap Fin) [A, x] \subseteq ⋃ z\} \to \exists z \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ z$
17	11 16	syl	$⊢ (((A \in ℝ \land B \in ℝ) \land A \leq B) \land (u \in 𝒫 J \land [A, B] \subseteq ⋃ u)) \to \exists z \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ z$
18	17	expr	$⊢ (((A \in ℝ \land B \in ℝ) \land A \leq B) \land u \in 𝒫 J) \to ([A, B] \subseteq ⋃ u \to \exists z \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ z)$
19	18	ralrimiva	$⊢ ((A \in ℝ \land B \in ℝ) \land A \leq B) \to \forall u \in 𝒫 J ([A, B] \subseteq ⋃ u \to \exists z \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ z)$
20		retop	$⊢ topGen (ran (.)) \in Top$
21	1 20	eqeltri	$⊢ J \in Top$
22		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
23	22	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land A \leq B) \to [A, B] \subseteq ℝ$
24		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
25	1	unieqi	$⊢ ⋃ J = ⋃ topGen (ran (.))$
26	24 25	eqtr4i	$⊢ ℝ = ⋃ J$
27	26	cmpsub	$⊢ (J \in Top \land [A, B] \subseteq ℝ) \to (J ↾_{𝑡} [A, B] \in Comp \leftrightarrow \forall u \in 𝒫 J ([A, B] \subseteq ⋃ u \to \exists z \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ z))$
28	21 23 27	sylancr	$⊢ ((A \in ℝ \land B \in ℝ) \land A \leq B) \to (J ↾_{𝑡} [A, B] \in Comp \leftrightarrow \forall u \in 𝒫 J ([A, B] \subseteq ⋃ u \to \exists z \in (𝒫 u \cap Fin) [A, B] \subseteq ⋃ z))$
29	19 28	mpbird	$⊢ ((A \in ℝ \land B \in ℝ) \land A \leq B) \to J ↾_{𝑡} [A, B] \in Comp$
30		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
31		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
32		icc0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B] = \emptyset \leftrightarrow B < A)$
33	30 31 32	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to ([A, B] = \emptyset \leftrightarrow B < A)$
34	33	biimpar	$⊢ ((A \in ℝ \land B \in ℝ) \land B < A) \to [A, B] = \emptyset$
35	34	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land B < A) \to J ↾_{𝑡} [A, B] = J ↾_{𝑡} \emptyset$
36		rest0	$⊢ J \in Top \to J ↾_{𝑡} \emptyset = \{\emptyset\}$
37	21 36	ax-mp	$⊢ J ↾_{𝑡} \emptyset = \{\emptyset\}$
38	35 37	syl6eq	$⊢ ((A \in ℝ \land B \in ℝ) \land B < A) \to J ↾_{𝑡} [A, B] = \{\emptyset\}$
39		0cmp	$⊢ \{\emptyset\} \in Comp$
40	38 39	eqeltrdi	$⊢ ((A \in ℝ \land B \in ℝ) \land B < A) \to J ↾_{𝑡} [A, B] \in Comp$
41		lelttric	$⊢ (A \in ℝ \land B \in ℝ) \to (A \leq B \lor B < A)$
42	29 40 41	mpjaodan	$⊢ (A \in ℝ \land B \in ℝ) \to J ↾_{𝑡} [A, B] \in Comp$
43	2 42	eqeltrid	$⊢ (A \in ℝ \land B \in ℝ) \to T \in Comp$

Metamath Proof Explorer

Theorem icccmp

Proof