rrnheibor

Description: Heine-Borel theorem for Euclidean space. A subset of Euclidean space is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	rrnheibor.1	$⊢ X = ℝ^{I}$
	rrnheibor.2	$⊢ M = {ℝ^{n} (I) ↾}_{(Y \times Y)}$
	rrnheibor.3	$⊢ T = MetOpen (M)$
	rrnheibor.4	$⊢ U = MetOpen (ℝ^{n} (I))$
Assertion	rrnheibor	$⊢ (I \in Fin \land Y \subseteq X) \to (T \in Comp \leftrightarrow (Y \in Clsd (U) \land M \in Bnd (Y)))$

Proof

Step	Hyp	Ref	Expression
1		rrnheibor.1	$⊢ X = ℝ^{I}$
2		rrnheibor.2	$⊢ M = {ℝ^{n} (I) ↾}_{(Y \times Y)}$
3		rrnheibor.3	$⊢ T = MetOpen (M)$
4		rrnheibor.4	$⊢ U = MetOpen (ℝ^{n} (I))$
5	1	rrnmet	$⊢ I \in Fin \to ℝ^{n} (I) \in Met (X)$
6		metres2	$⊢ (ℝ^{n} (I) \in Met (X) \land Y \subseteq X) \to {ℝ^{n} (I) ↾}_{(Y \times Y)} \in Met (Y)$
7	2 6	eqeltrid	$⊢ (ℝ^{n} (I) \in Met (X) \land Y \subseteq X) \to M \in Met (Y)$
8	5 7	sylan	$⊢ (I \in Fin \land Y \subseteq X) \to M \in Met (Y)$
9	8	biantrurd	$⊢ (I \in Fin \land Y \subseteq X) \to (T \in Comp \leftrightarrow (M \in Met (Y) \land T \in Comp))$
10	3	heibor	$⊢ (M \in Met (Y) \land T \in Comp) \leftrightarrow (M \in CMet (Y) \land M \in TotBnd (Y))$
11	9 10	bitrdi	$⊢ (I \in Fin \land Y \subseteq X) \to (T \in Comp \leftrightarrow (M \in CMet (Y) \land M \in TotBnd (Y)))$
12	2	eleq1i	$⊢ M \in CMet (Y) \leftrightarrow {ℝ^{n} (I) ↾}_{(Y \times Y)} \in CMet (Y)$
13	1	rrncms	$⊢ I \in Fin \to ℝ^{n} (I) \in CMet (X)$
14	13	adantr	$⊢ (I \in Fin \land Y \subseteq X) \to ℝ^{n} (I) \in CMet (X)$
15	4	cmetss	$⊢ ℝ^{n} (I) \in CMet (X) \to ({ℝ^{n} (I) ↾}_{(Y \times Y)} \in CMet (Y) \leftrightarrow Y \in Clsd (U))$
16	14 15	syl	$⊢ (I \in Fin \land Y \subseteq X) \to ({ℝ^{n} (I) ↾}_{(Y \times Y)} \in CMet (Y) \leftrightarrow Y \in Clsd (U))$
17	12 16	bitrid	$⊢ (I \in Fin \land Y \subseteq X) \to (M \in CMet (Y) \leftrightarrow Y \in Clsd (U))$
18	1 2	rrntotbnd	$⊢ I \in Fin \to (M \in TotBnd (Y) \leftrightarrow M \in Bnd (Y))$
19	18	adantr	$⊢ (I \in Fin \land Y \subseteq X) \to (M \in TotBnd (Y) \leftrightarrow M \in Bnd (Y))$
20	17 19	anbi12d	$⊢ (I \in Fin \land Y \subseteq X) \to ((M \in CMet (Y) \land M \in TotBnd (Y)) \leftrightarrow (Y \in Clsd (U) \land M \in Bnd (Y)))$
21	11 20	bitrd	$⊢ (I \in Fin \land Y \subseteq X) \to (T \in Comp \leftrightarrow (Y \in Clsd (U) \land M \in Bnd (Y)))$

Metamath Proof Explorer

Theorem rrnheibor

Proof