heibor1

Description: One half of heibor , that does not require any Choice. A compact metric space is complete and totally bounded. We prove completeness in cmpcmet and total boundedness here, which follows trivially from the fact that the set of all r -balls is an open cover of X , so finitely many cover X . (Contributed by Jeff Madsen, 16-Jan-2014)

		Ref	Expression
	Hypothesis	heibor.1	$⊢ J = MetOpen (D)$
	Assertion	heibor1	$⊢ (D \in Met (X) \land J \in Comp) \to (D \in CMet (X) \land D \in TotBnd (X))$

Proof

Step	Hyp	Ref	Expression
1		heibor.1	$⊢ J = MetOpen (D)$
2		simpll	$⊢ ((D \in Met (X) \land J \in Comp) \land (x \in Cau (D) \land x : ℕ ⟶ X)) \to D \in Met (X)$
3		simplr	$⊢ ((D \in Met (X) \land J \in Comp) \land (x \in Cau (D) \land x : ℕ ⟶ X)) \to J \in Comp$
4		simprl	$⊢ ((D \in Met (X) \land J \in Comp) \land (x \in Cau (D) \land x : ℕ ⟶ X)) \to x \in Cau (D)$
5		simprr	$⊢ ((D \in Met (X) \land J \in Comp) \land (x \in Cau (D) \land x : ℕ ⟶ X)) \to x : ℕ ⟶ X$
6	1 2 3 4 5	heibor1lem	$⊢ ((D \in Met (X) \land J \in Comp) \land (x \in Cau (D) \land x : ℕ ⟶ X)) \to x \in dom \underset{t}{⇝} (J)$
7	6	expr	$⊢ ((D \in Met (X) \land J \in Comp) \land x \in Cau (D)) \to (x : ℕ ⟶ X \to x \in dom \underset{t}{⇝} (J))$
8	7	ralrimiva	$⊢ (D \in Met (X) \land J \in Comp) \to \forall x \in Cau (D) (x : ℕ ⟶ X \to x \in dom \underset{t}{⇝} (J))$
9		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
10		1zzd	$⊢ (D \in Met (X) \land J \in Comp) \to 1 \in ℤ$
11		simpl	$⊢ (D \in Met (X) \land J \in Comp) \to D \in Met (X)$
12	9 1 10 11	iscmet3	$⊢ (D \in Met (X) \land J \in Comp) \to (D \in CMet (X) \leftrightarrow \forall x \in Cau (D) (x : ℕ ⟶ X \to x \in dom \underset{t}{⇝} (J)))$
13	8 12	mpbird	$⊢ (D \in Met (X) \land J \in Comp) \to D \in CMet (X)$
14		simplr	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to J \in Comp$
15		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
16		id	$⊢ z \in X \to z \in X$
17		rpxr	$⊢ r \in ℝ^{+} \to r \in ℝ^{*}$
18	1	blopn	$⊢ (D \in ∞Met (X) \land z \in X \land r \in ℝ^{*}) \to z ball (D) r \in J$
19	15 16 17 18	syl3an	$⊢ (D \in Met (X) \land z \in X \land r \in ℝ^{+}) \to z ball (D) r \in J$
20	19	3com23	$⊢ (D \in Met (X) \land r \in ℝ^{+} \land z \in X) \to z ball (D) r \in J$
21	20	3expa	$⊢ ((D \in Met (X) \land r \in ℝ^{+}) \land z \in X) \to z ball (D) r \in J$
22		eleq1a	$⊢ z ball (D) r \in J \to (y = z ball (D) r \to y \in J)$
23	21 22	syl	$⊢ ((D \in Met (X) \land r \in ℝ^{+}) \land z \in X) \to (y = z ball (D) r \to y \in J)$
24	23	rexlimdva	$⊢ (D \in Met (X) \land r \in ℝ^{+}) \to (\exists z \in X y = z ball (D) r \to y \in J)$
25	24	adantlr	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to (\exists z \in X y = z ball (D) r \to y \in J)$
26	25	abssdv	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to \{y \| \exists z \in X y = z ball (D) r\} \subseteq J$
27	15	ad2antrr	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to D \in ∞Met (X)$
28	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
29	27 28	syl	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to X = ⋃ J$
30		blcntr	$⊢ (D \in ∞Met (X) \land z \in X \land r \in ℝ^{+}) \to z \in (z ball (D) r)$
31	15 30	syl3an1	$⊢ (D \in Met (X) \land z \in X \land r \in ℝ^{+}) \to z \in (z ball (D) r)$
32	31	3com23	$⊢ (D \in Met (X) \land r \in ℝ^{+} \land z \in X) \to z \in (z ball (D) r)$
33	32	3expa	$⊢ ((D \in Met (X) \land r \in ℝ^{+}) \land z \in X) \to z \in (z ball (D) r)$
34		ovex	$⊢ z ball (D) r \in V$
35	34	elabrex	$⊢ z \in X \to z ball (D) r \in \{y \| \exists z \in X y = z ball (D) r\}$
36	35	adantl	$⊢ ((D \in Met (X) \land r \in ℝ^{+}) \land z \in X) \to z ball (D) r \in \{y \| \exists z \in X y = z ball (D) r\}$
37		elunii	$⊢ (z \in (z ball (D) r) \land z ball (D) r \in \{y \| \exists z \in X y = z ball (D) r\}) \to z \in ⋃ \{y \| \exists z \in X y = z ball (D) r\}$
38	33 36 37	syl2anc	$⊢ ((D \in Met (X) \land r \in ℝ^{+}) \land z \in X) \to z \in ⋃ \{y \| \exists z \in X y = z ball (D) r\}$
39	38	ralrimiva	$⊢ (D \in Met (X) \land r \in ℝ^{+}) \to \forall z \in X z \in ⋃ \{y \| \exists z \in X y = z ball (D) r\}$
40	39	adantlr	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to \forall z \in X z \in ⋃ \{y \| \exists z \in X y = z ball (D) r\}$
41		nfcv	$⊢ \underline{Ⅎ} z X$
42		nfre1	$⊢ Ⅎ z \exists z \in X y = z ball (D) r$
43	42	nfab	$⊢ \underline{Ⅎ} z \{y \| \exists z \in X y = z ball (D) r\}$
44	43	nfuni	$⊢ \underline{Ⅎ} z ⋃ \{y \| \exists z \in X y = z ball (D) r\}$
45	41 44	dfss3f	$⊢ X \subseteq ⋃ \{y \| \exists z \in X y = z ball (D) r\} \leftrightarrow \forall z \in X z \in ⋃ \{y \| \exists z \in X y = z ball (D) r\}$
46	40 45	sylibr	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to X \subseteq ⋃ \{y \| \exists z \in X y = z ball (D) r\}$
47	29 46	eqsstrrd	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to ⋃ J \subseteq ⋃ \{y \| \exists z \in X y = z ball (D) r\}$
48	26	unissd	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to ⋃ \{y \| \exists z \in X y = z ball (D) r\} \subseteq ⋃ J$
49	47 48	eqssd	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to ⋃ J = ⋃ \{y \| \exists z \in X y = z ball (D) r\}$
50		eqid	$⊢ ⋃ J = ⋃ J$
51	50	cmpcov	$⊢ (J \in Comp \land \{y \| \exists z \in X y = z ball (D) r\} \subseteq J \land ⋃ J = ⋃ \{y \| \exists z \in X y = z ball (D) r\}) \to \exists x \in (𝒫 \{y \| \exists z \in X y = z ball (D) r\} \cap Fin) ⋃ J = ⋃ x$
52	14 26 49 51	syl3anc	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to \exists x \in (𝒫 \{y \| \exists z \in X y = z ball (D) r\} \cap Fin) ⋃ J = ⋃ x$
53		elin	$⊢ x \in (𝒫 \{y \| \exists z \in X y = z ball (D) r\} \cap Fin) \leftrightarrow (x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\} \land x \in Fin)$
54		ancom	$⊢ (x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\} \land x \in Fin) \leftrightarrow (x \in Fin \land x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\})$
55	53 54	bitri	$⊢ x \in (𝒫 \{y \| \exists z \in X y = z ball (D) r\} \cap Fin) \leftrightarrow (x \in Fin \land x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\})$
56	55	anbi1i	$⊢ (x \in (𝒫 \{y \| \exists z \in X y = z ball (D) r\} \cap Fin) \land ⋃ J = ⋃ x) \leftrightarrow ((x \in Fin \land x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\}) \land ⋃ J = ⋃ x)$
57		anass	$⊢ ((x \in Fin \land x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\}) \land ⋃ J = ⋃ x) \leftrightarrow (x \in Fin \land (x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\} \land ⋃ J = ⋃ x))$
58	56 57	bitri	$⊢ (x \in (𝒫 \{y \| \exists z \in X y = z ball (D) r\} \cap Fin) \land ⋃ J = ⋃ x) \leftrightarrow (x \in Fin \land (x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\} \land ⋃ J = ⋃ x))$
59	58	rexbii2	$⊢ \exists x \in (𝒫 \{y \| \exists z \in X y = z ball (D) r\} \cap Fin) ⋃ J = ⋃ x \leftrightarrow \exists x \in Fin (x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\} \land ⋃ J = ⋃ x)$
60	52 59	sylib	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to \exists x \in Fin (x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\} \land ⋃ J = ⋃ x)$
61		ancom	$⊢ (x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\} \land ⋃ J = ⋃ x) \leftrightarrow (⋃ J = ⋃ x \land x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\})$
62		eqcom	$⊢ ⋃ x = X \leftrightarrow X = ⋃ x$
63	29	eqeq1d	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to (X = ⋃ x \leftrightarrow ⋃ J = ⋃ x)$
64	62 63	bitr2id	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to (⋃ J = ⋃ x \leftrightarrow ⋃ x = X)$
65	64	anbi1d	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to ((⋃ J = ⋃ x \land x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\}) \leftrightarrow (⋃ x = X \land x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\}))$
66	61 65	syl5bb	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to ((x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\} \land ⋃ J = ⋃ x) \leftrightarrow (⋃ x = X \land x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\}))$
67		elpwi	$⊢ x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\} \to x \subseteq \{y \| \exists z \in X y = z ball (D) r\}$
68		ssabral	$⊢ x \subseteq \{y \| \exists z \in X y = z ball (D) r\} \leftrightarrow \forall y \in x \exists z \in X y = z ball (D) r$
69	67 68	sylib	$⊢ x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\} \to \forall y \in x \exists z \in X y = z ball (D) r$
70	69	anim2i	$⊢ (⋃ x = X \land x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\}) \to (⋃ x = X \land \forall y \in x \exists z \in X y = z ball (D) r)$
71	66 70	syl6bi	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to ((x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\} \land ⋃ J = ⋃ x) \to (⋃ x = X \land \forall y \in x \exists z \in X y = z ball (D) r))$
72	71	reximdv	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to (\exists x \in Fin (x \in 𝒫 \{y \| \exists z \in X y = z ball (D) r\} \land ⋃ J = ⋃ x) \to \exists x \in Fin (⋃ x = X \land \forall y \in x \exists z \in X y = z ball (D) r))$
73	60 72	mpd	$⊢ ((D \in Met (X) \land J \in Comp) \land r \in ℝ^{+}) \to \exists x \in Fin (⋃ x = X \land \forall y \in x \exists z \in X y = z ball (D) r)$
74	73	ralrimiva	$⊢ (D \in Met (X) \land J \in Comp) \to \forall r \in ℝ^{+} \exists x \in Fin (⋃ x = X \land \forall y \in x \exists z \in X y = z ball (D) r)$
75		istotbnd	$⊢ D \in TotBnd (X) \leftrightarrow (D \in Met (X) \land \forall r \in ℝ^{+} \exists x \in Fin (⋃ x = X \land \forall y \in x \exists z \in X y = z ball (D) r))$
76	11 74 75	sylanbrc	$⊢ (D \in Met (X) \land J \in Comp) \to D \in TotBnd (X)$
77	13 76	jca	$⊢ (D \in Met (X) \land J \in Comp) \to (D \in CMet (X) \land D \in TotBnd (X))$

Metamath Proof Explorer

Theorem heibor1

Proof