reheibor

Description: Heine-Borel theorem for real numbers. A subset of RR 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	reheibor.2	$⊢ M = {(abs \circ -) ↾}_{(Y \times Y)}$
	reheibor.3	$⊢ T = MetOpen (M)$
	reheibor.4	$⊢ U = topGen (ran (.))$
Assertion	reheibor	$⊢ Y \subseteq ℝ \to (T \in Comp \leftrightarrow (Y \in Clsd (U) \land M \in Bnd (Y)))$

Proof

Step	Hyp	Ref	Expression
1		reheibor.2	$⊢ M = {(abs \circ -) ↾}_{(Y \times Y)}$
2		reheibor.3	$⊢ T = MetOpen (M)$
3		reheibor.4	$⊢ U = topGen (ran (.))$
4		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
5		snfi	$⊢ \{\emptyset\} \in Fin$
6	4 5	eqeltri	$⊢ 1_{𝑜} \in Fin$
7		imassrn	$⊢ (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \subseteq ran (x \in ℝ ⟼ \{\emptyset\} \times \{x\})$
8		0ex	$⊢ \emptyset \in V$
9		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
10		eqid	$⊢ (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) = (x \in ℝ ⟼ \{\emptyset\} \times \{x\})$
11	9 10	ismrer1	$⊢ \emptyset \in V \to (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) \in (({(abs \circ -) ↾}_{ℝ^{2}}) Ismty ℝ^{n} (\{\emptyset\}))$
12	8 11	ax-mp	$⊢ (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) \in (({(abs \circ -) ↾}_{ℝ^{2}}) Ismty ℝ^{n} (\{\emptyset\}))$
13	4	fveq2i	$⊢ ℝ^{n} (1_{𝑜}) = ℝ^{n} (\{\emptyset\})$
14	13	oveq2i	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}}) Ismty ℝ^{n} (1_{𝑜}) = ({(abs \circ -) ↾}_{ℝ^{2}}) Ismty ℝ^{n} (\{\emptyset\})$
15	12 14	eleqtrri	$⊢ (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) \in (({(abs \circ -) ↾}_{ℝ^{2}}) Ismty ℝ^{n} (1_{𝑜}))$
16	9	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
17		eqid	$⊢ ℝ^{1_{𝑜}} = ℝ^{1_{𝑜}}$
18	17	rrnmet	$⊢ 1_{𝑜} \in Fin \to ℝ^{n} (1_{𝑜}) \in Met (ℝ^{1_{𝑜}})$
19		metxmet	$⊢ ℝ^{n} (1_{𝑜}) \in Met (ℝ^{1_{𝑜}}) \to ℝ^{n} (1_{𝑜}) \in ∞Met (ℝ^{1_{𝑜}})$
20	6 18 19	mp2b	$⊢ ℝ^{n} (1_{𝑜}) \in ∞Met (ℝ^{1_{𝑜}})$
21		isismty	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land ℝ^{n} (1_{𝑜}) \in ∞Met (ℝ^{1_{𝑜}})) \to ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) \in (({(abs \circ -) ↾}_{ℝ^{2}}) Ismty ℝ^{n} (1_{𝑜})) \leftrightarrow ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) : ℝ \underset{1-1 onto}{⟶} ℝ^{1_{𝑜}} \land \forall y \in ℝ \forall z \in ℝ y ({(abs \circ -) ↾}_{ℝ^{2}}) z = (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) (y) ℝ^{n} (1_{𝑜}) (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) (z)))$
22	16 20 21	mp2an	$⊢ (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) \in (({(abs \circ -) ↾}_{ℝ^{2}}) Ismty ℝ^{n} (1_{𝑜})) \leftrightarrow ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) : ℝ \underset{1-1 onto}{⟶} ℝ^{1_{𝑜}} \land \forall y \in ℝ \forall z \in ℝ y ({(abs \circ -) ↾}_{ℝ^{2}}) z = (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) (y) ℝ^{n} (1_{𝑜}) (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) (z))$
23	15 22	mpbi	$⊢ ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) : ℝ \underset{1-1 onto}{⟶} ℝ^{1_{𝑜}} \land \forall y \in ℝ \forall z \in ℝ y ({(abs \circ -) ↾}_{ℝ^{2}}) z = (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) (y) ℝ^{n} (1_{𝑜}) (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) (z))$
24	23	simpli	$⊢ (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) : ℝ \underset{1-1 onto}{⟶} ℝ^{1_{𝑜}}$
25		f1of	$⊢ (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) : ℝ \underset{1-1 onto}{⟶} ℝ^{1_{𝑜}} \to (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) : ℝ ⟶ ℝ^{1_{𝑜}}$
26		frn	$⊢ (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) : ℝ ⟶ ℝ^{1_{𝑜}} \to ran (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) \subseteq ℝ^{1_{𝑜}}$
27	24 25 26	mp2b	$⊢ ran (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) \subseteq ℝ^{1_{𝑜}}$
28	7 27	sstri	$⊢ (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \subseteq ℝ^{1_{𝑜}}$
29	28	a1i	$⊢ Y \subseteq ℝ \to (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \subseteq ℝ^{1_{𝑜}}$
30		eqid	$⊢ {ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])} = {ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}$
31		eqid	$⊢ MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) = MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])})$
32		eqid	$⊢ MetOpen (ℝ^{n} (1_{𝑜})) = MetOpen (ℝ^{n} (1_{𝑜}))$
33	17 30 31 32	rrnheibor	$⊢ (1_{𝑜} \in Fin \land (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \subseteq ℝ^{1_{𝑜}}) \to (MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) \in Comp \leftrightarrow ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \in Clsd (MetOpen (ℝ^{n} (1_{𝑜}))) \land {ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])} \in Bnd ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])))$
34	6 29 33	sylancr	$⊢ Y \subseteq ℝ \to (MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) \in Comp \leftrightarrow ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \in Clsd (MetOpen (ℝ^{n} (1_{𝑜}))) \land {ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])} \in Bnd ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])))$
35		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
36		id	$⊢ Y \subseteq ℝ \to Y \subseteq ℝ$
37		ax-resscn	$⊢ ℝ \subseteq ℂ$
38	36 37	sstrdi	$⊢ Y \subseteq ℝ \to Y \subseteq ℂ$
39		xmetres2	$⊢ (abs \circ - \in ∞Met (ℂ) \land Y \subseteq ℂ) \to {(abs \circ -) ↾}_{(Y \times Y)} \in ∞Met (Y)$
40	35 38 39	sylancr	$⊢ Y \subseteq ℝ \to {(abs \circ -) ↾}_{(Y \times Y)} \in ∞Met (Y)$
41	1 40	eqeltrid	$⊢ Y \subseteq ℝ \to M \in ∞Met (Y)$
42		xmetres2	$⊢ (ℝ^{n} (1_{𝑜}) \in ∞Met (ℝ^{1_{𝑜}}) \land (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \subseteq ℝ^{1_{𝑜}}) \to {ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])} \in ∞Met ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])$
43	20 29 42	sylancr	$⊢ Y \subseteq ℝ \to {ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])} \in ∞Met ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])$
44	2 31	ismtyhmeo	$⊢ (M \in ∞Met (Y) \land {ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])} \in ∞Met ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])) \to M Ismty ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) \subseteq T Homeo MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])})$
45	41 43 44	syl2anc	$⊢ Y \subseteq ℝ \to M Ismty ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) \subseteq T Homeo MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])})$
46	16	a1i	$⊢ Y \subseteq ℝ \to {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
47	20	a1i	$⊢ Y \subseteq ℝ \to ℝ^{n} (1_{𝑜}) \in ∞Met (ℝ^{1_{𝑜}})$
48	15	a1i	$⊢ Y \subseteq ℝ \to (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) \in (({(abs \circ -) ↾}_{ℝ^{2}}) Ismty ℝ^{n} (1_{𝑜}))$
49		eqid	$⊢ (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] = (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y]$
50		eqid	$⊢ {({(abs \circ -) ↾}_{ℝ^{2}}) ↾}_{(Y \times Y)} = {({(abs \circ -) ↾}_{ℝ^{2}}) ↾}_{(Y \times Y)}$
51	49 50 30	ismtyres	$⊢ (({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land ℝ^{n} (1_{𝑜}) \in ∞Met (ℝ^{1_{𝑜}})) \land ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) \in (({(abs \circ -) ↾}_{ℝ^{2}}) Ismty ℝ^{n} (1_{𝑜})) \land Y \subseteq ℝ)) \to {(x \in ℝ ⟼ \{\emptyset\} \times \{x\}) ↾}_{Y} \in (({({(abs \circ -) ↾}_{ℝ^{2}}) ↾}_{(Y \times Y)}) Ismty ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}))$
52	46 47 48 36 51	syl22anc	$⊢ Y \subseteq ℝ \to {(x \in ℝ ⟼ \{\emptyset\} \times \{x\}) ↾}_{Y} \in (({({(abs \circ -) ↾}_{ℝ^{2}}) ↾}_{(Y \times Y)}) Ismty ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}))$
53		xpss12	$⊢ (Y \subseteq ℝ \land Y \subseteq ℝ) \to Y \times Y \subseteq ℝ^{2}$
54	53	anidms	$⊢ Y \subseteq ℝ \to Y \times Y \subseteq ℝ^{2}$
55	54	resabs1d	$⊢ Y \subseteq ℝ \to {({(abs \circ -) ↾}_{ℝ^{2}}) ↾}_{(Y \times Y)} = {(abs \circ -) ↾}_{(Y \times Y)}$
56	55 1	eqtr4di	$⊢ Y \subseteq ℝ \to {({(abs \circ -) ↾}_{ℝ^{2}}) ↾}_{(Y \times Y)} = M$
57	56	oveq1d	$⊢ Y \subseteq ℝ \to ({({(abs \circ -) ↾}_{ℝ^{2}}) ↾}_{(Y \times Y)}) Ismty ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) = M Ismty ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])})$
58	52 57	eleqtrd	$⊢ Y \subseteq ℝ \to {(x \in ℝ ⟼ \{\emptyset\} \times \{x\}) ↾}_{Y} \in (M Ismty ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}))$
59	45 58	sseldd	$⊢ Y \subseteq ℝ \to {(x \in ℝ ⟼ \{\emptyset\} \times \{x\}) ↾}_{Y} \in (T Homeo MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}))$
60		hmphi	$⊢ {(x \in ℝ ⟼ \{\emptyset\} \times \{x\}) ↾}_{Y} \in (T Homeo MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])})) \to T ≃ MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])})$
61	59 60	syl	$⊢ Y \subseteq ℝ \to T ≃ MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])})$
62		cmphmph	$⊢ T ≃ MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) \to (T \in Comp \to MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) \in Comp)$
63		hmphsym	$⊢ T ≃ MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) \to MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) ≃ T$
64		cmphmph	$⊢ MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) ≃ T \to (MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) \in Comp \to T \in Comp)$
65	63 64	syl	$⊢ T ≃ MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) \to (MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) \in Comp \to T \in Comp)$
66	62 65	impbid	$⊢ T ≃ MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) \to (T \in Comp \leftrightarrow MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) \in Comp)$
67	61 66	syl	$⊢ Y \subseteq ℝ \to (T \in Comp \leftrightarrow MetOpen ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}) \in Comp)$
68		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
69	9 68	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
70	3 69	eqtri	$⊢ U = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
71	70 32	ismtyhmeo	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land ℝ^{n} (1_{𝑜}) \in ∞Met (ℝ^{1_{𝑜}})) \to ({(abs \circ -) ↾}_{ℝ^{2}}) Ismty ℝ^{n} (1_{𝑜}) \subseteq U Homeo MetOpen (ℝ^{n} (1_{𝑜}))$
72	16 20 71	mp2an	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}}) Ismty ℝ^{n} (1_{𝑜}) \subseteq U Homeo MetOpen (ℝ^{n} (1_{𝑜}))$
73	72 15	sselii	$⊢ (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) \in (U Homeo MetOpen (ℝ^{n} (1_{𝑜})))$
74		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
75	3 74	eqeltri	$⊢ U \in TopOn (ℝ)$
76	75	toponunii	$⊢ ℝ = ⋃ U$
77	76	hmeocld	$⊢ ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) \in (U Homeo MetOpen (ℝ^{n} (1_{𝑜}))) \land Y \subseteq ℝ) \to (Y \in Clsd (U) \leftrightarrow (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \in Clsd (MetOpen (ℝ^{n} (1_{𝑜}))))$
78	73 36 77	sylancr	$⊢ Y \subseteq ℝ \to (Y \in Clsd (U) \leftrightarrow (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \in Clsd (MetOpen (ℝ^{n} (1_{𝑜}))))$
79		ismtybnd	$⊢ (M \in ∞Met (Y) \land {ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])} \in ∞Met ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y]) \land {(x \in ℝ ⟼ \{\emptyset\} \times \{x\}) ↾}_{Y} \in (M Ismty ({ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])}))) \to (M \in Bnd (Y) \leftrightarrow {ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])} \in Bnd ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y]))$
80	41 43 58 79	syl3anc	$⊢ Y \subseteq ℝ \to (M \in Bnd (Y) \leftrightarrow {ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])} \in Bnd ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y]))$
81	78 80	anbi12d	$⊢ Y \subseteq ℝ \to ((Y \in Clsd (U) \land M \in Bnd (Y)) \leftrightarrow ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \in Clsd (MetOpen (ℝ^{n} (1_{𝑜}))) \land {ℝ^{n} (1_{𝑜}) ↾}_{((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y] \times (x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])} \in Bnd ((x \in ℝ ⟼ \{\emptyset\} \times \{x\}) [Y])))$
82	34 67 81	3bitr4d	$⊢ Y \subseteq ℝ \to (T \in Comp \leftrightarrow (Y \in Clsd (U) \land M \in Bnd (Y)))$

Metamath Proof Explorer

Theorem reheibor

Proof