heibor

Description: Generalized Heine-Borel Theorem. A metric space is compact iff it is complete and totally bounded. See heibor1 and heiborlem1 for a description of the proof. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 28-Jan-2014)

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

Proof

Step	Hyp	Ref	Expression
1		heibor.1	$⊢ J = MetOpen (D)$
2	1	heibor1	$⊢ (D \in Met (X) \land J \in Comp) \to (D \in CMet (X) \land D \in TotBnd (X))$
3		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
4	3	adantr	$⊢ (D \in CMet (X) \land D \in TotBnd (X)) \to D \in Met (X)$
5		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
6	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
7	3 5 6	3syl	$⊢ D \in CMet (X) \to J \in Top$
8	7	adantr	$⊢ (D \in CMet (X) \land D \in TotBnd (X)) \to J \in Top$
9		istotbnd	$⊢ D \in TotBnd (X) \leftrightarrow (D \in Met (X) \land \forall r \in ℝ^{+} \exists u \in Fin (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) r))$
10	9	simprbi	$⊢ D \in TotBnd (X) \to \forall r \in ℝ^{+} \exists u \in Fin (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) r)$
11		2nn	$⊢ 2 \in ℕ$
12		nnexpcl	$⊢ (2 \in ℕ \land n \in ℕ_{0}) \to 2^{n} \in ℕ$
13	11 12	mpan	$⊢ n \in ℕ_{0} \to 2^{n} \in ℕ$
14	13	nnrpd	$⊢ n \in ℕ_{0} \to 2^{n} \in ℝ^{+}$
15	14	rpreccld	$⊢ n \in ℕ_{0} \to \frac{1}{2^{n}} \in ℝ^{+}$
16		oveq2	$⊢ r = \frac{1}{2^{n}} \to y ball (D) r = y ball (D) (\frac{1}{2^{n}})$
17	16	eqeq2d	$⊢ r = \frac{1}{2^{n}} \to (v = y ball (D) r \leftrightarrow v = y ball (D) (\frac{1}{2^{n}}))$
18	17	rexbidv	$⊢ r = \frac{1}{2^{n}} \to (\exists y \in X v = y ball (D) r \leftrightarrow \exists y \in X v = y ball (D) (\frac{1}{2^{n}}))$
19	18	ralbidv	$⊢ r = \frac{1}{2^{n}} \to (\forall v \in u \exists y \in X v = y ball (D) r \leftrightarrow \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}}))$
20	19	anbi2d	$⊢ r = \frac{1}{2^{n}} \to ((⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) r) \leftrightarrow (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}})))$
21	20	rexbidv	$⊢ r = \frac{1}{2^{n}} \to (\exists u \in Fin (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) r) \leftrightarrow \exists u \in Fin (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}})))$
22	21	rspccva	$⊢ (\forall r \in ℝ^{+} \exists u \in Fin (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) r) \land \frac{1}{2^{n}} \in ℝ^{+}) \to \exists u \in Fin (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}}))$
23	10 15 22	syl2an	$⊢ (D \in TotBnd (X) \land n \in ℕ_{0}) \to \exists u \in Fin (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}}))$
24	23	expcom	$⊢ n \in ℕ_{0} \to (D \in TotBnd (X) \to \exists u \in Fin (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}})))$
25	24	adantl	$⊢ (D \in CMet (X) \land n \in ℕ_{0}) \to (D \in TotBnd (X) \to \exists u \in Fin (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}})))$
26		oveq1	$⊢ y = m (v) \to y ball (D) (\frac{1}{2^{n}}) = m (v) ball (D) (\frac{1}{2^{n}})$
27	26	eqeq2d	$⊢ y = m (v) \to (v = y ball (D) (\frac{1}{2^{n}}) \leftrightarrow v = m (v) ball (D) (\frac{1}{2^{n}}))$
28	27	ac6sfi	$⊢ (u \in Fin \land \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}})) \to \exists m (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))$
29	28	adantrl	$⊢ (u \in Fin \land (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}}))) \to \exists m (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))$
30	29	adantl	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}})))) \to \exists m (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))$
31		simp3l	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to m : u ⟶ X$
32	31	frnd	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to ran m \subseteq X$
33	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
34	3 5 33	3syl	$⊢ D \in CMet (X) \to X = ⋃ J$
35	34	adantr	$⊢ (D \in CMet (X) \land n \in ℕ_{0}) \to X = ⋃ J$
36	35	3ad2ant1	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to X = ⋃ J$
37	32 36	sseqtrd	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to ran m \subseteq ⋃ J$
38	1	fvexi	$⊢ J \in V$
39	38	uniex	$⊢ ⋃ J \in V$
40	39	elpw2	$⊢ ran m \in 𝒫 ⋃ J \leftrightarrow ran m \subseteq ⋃ J$
41	37 40	sylibr	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to ran m \in 𝒫 ⋃ J$
42		simp2l	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to u \in Fin$
43		ffn	$⊢ m : u ⟶ X \to m Fn u$
44		dffn4	$⊢ m Fn u \leftrightarrow m : u \underset{onto}{⟶} ran m$
45	43 44	sylib	$⊢ m : u ⟶ X \to m : u \underset{onto}{⟶} ran m$
46		fofi	$⊢ (u \in Fin \land m : u \underset{onto}{⟶} ran m) \to ran m \in Fin$
47	45 46	sylan2	$⊢ (u \in Fin \land m : u ⟶ X) \to ran m \in Fin$
48	42 31 47	syl2anc	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to ran m \in Fin$
49	41 48	elind	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to ran m \in (𝒫 ⋃ J \cap Fin)$
50	26	eleq2d	$⊢ y = m (v) \to (r \in (y ball (D) (\frac{1}{2^{n}})) \leftrightarrow r \in (m (v) ball (D) (\frac{1}{2^{n}})))$
51	50	rexrn	$⊢ m Fn u \to (\exists y \in ran m r \in (y ball (D) (\frac{1}{2^{n}})) \leftrightarrow \exists v \in u r \in (m (v) ball (D) (\frac{1}{2^{n}})))$
52		eliun	$⊢ r \in ⋃_{y \in ran m} (y ball (D) (\frac{1}{2^{n}})) \leftrightarrow \exists y \in ran m r \in (y ball (D) (\frac{1}{2^{n}}))$
53		eliun	$⊢ r \in ⋃_{v \in u} (m (v) ball (D) (\frac{1}{2^{n}})) \leftrightarrow \exists v \in u r \in (m (v) ball (D) (\frac{1}{2^{n}}))$
54	51 52 53	3bitr4g	$⊢ m Fn u \to (r \in ⋃_{y \in ran m} (y ball (D) (\frac{1}{2^{n}})) \leftrightarrow r \in ⋃_{v \in u} (m (v) ball (D) (\frac{1}{2^{n}})))$
55	54	eqrdv	$⊢ m Fn u \to ⋃_{y \in ran m} (y ball (D) (\frac{1}{2^{n}})) = ⋃_{v \in u} (m (v) ball (D) (\frac{1}{2^{n}}))$
56	31 43 55	3syl	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to ⋃_{y \in ran m} (y ball (D) (\frac{1}{2^{n}})) = ⋃_{v \in u} (m (v) ball (D) (\frac{1}{2^{n}}))$
57		simp3r	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}})$
58		uniiun	$⊢ ⋃ u = ⋃_{v \in u} v$
59		iuneq2	$⊢ \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}) \to ⋃_{v \in u} v = ⋃_{v \in u} (m (v) ball (D) (\frac{1}{2^{n}}))$
60	58 59	eqtrid	$⊢ \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}) \to ⋃ u = ⋃_{v \in u} (m (v) ball (D) (\frac{1}{2^{n}}))$
61	57 60	syl	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to ⋃ u = ⋃_{v \in u} (m (v) ball (D) (\frac{1}{2^{n}}))$
62		simp2r	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to ⋃ u = X$
63	56 61 62	3eqtr2rd	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to X = ⋃_{y \in ran m} (y ball (D) (\frac{1}{2^{n}}))$
64		iuneq1	$⊢ t = ran m \to ⋃_{y \in t} (y ball (D) (\frac{1}{2^{n}})) = ⋃_{y \in ran m} (y ball (D) (\frac{1}{2^{n}}))$
65	64	rspceeqv	$⊢ (ran m \in (𝒫 ⋃ J \cap Fin) \land X = ⋃_{y \in ran m} (y ball (D) (\frac{1}{2^{n}}))) \to \exists t \in (𝒫 ⋃ J \cap Fin) X = ⋃_{y \in t} (y ball (D) (\frac{1}{2^{n}}))$
66	49 63 65	syl2anc	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X) \land (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}}))) \to \exists t \in (𝒫 ⋃ J \cap Fin) X = ⋃_{y \in t} (y ball (D) (\frac{1}{2^{n}}))$
67	66	3expia	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land ⋃ u = X)) \to ((m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}})) \to \exists t \in (𝒫 ⋃ J \cap Fin) X = ⋃_{y \in t} (y ball (D) (\frac{1}{2^{n}})))$
68	67	adantrrr	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}})))) \to ((m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}})) \to \exists t \in (𝒫 ⋃ J \cap Fin) X = ⋃_{y \in t} (y ball (D) (\frac{1}{2^{n}})))$
69	68	exlimdv	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}})))) \to (\exists m (m : u ⟶ X \land \forall v \in u v = m (v) ball (D) (\frac{1}{2^{n}})) \to \exists t \in (𝒫 ⋃ J \cap Fin) X = ⋃_{y \in t} (y ball (D) (\frac{1}{2^{n}})))$
70	30 69	mpd	$⊢ ((D \in CMet (X) \land n \in ℕ_{0}) \land (u \in Fin \land (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}})))) \to \exists t \in (𝒫 ⋃ J \cap Fin) X = ⋃_{y \in t} (y ball (D) (\frac{1}{2^{n}}))$
71	70	rexlimdvaa	$⊢ (D \in CMet (X) \land n \in ℕ_{0}) \to (\exists u \in Fin (⋃ u = X \land \forall v \in u \exists y \in X v = y ball (D) (\frac{1}{2^{n}})) \to \exists t \in (𝒫 ⋃ J \cap Fin) X = ⋃_{y \in t} (y ball (D) (\frac{1}{2^{n}})))$
72	25 71	syld	$⊢ (D \in CMet (X) \land n \in ℕ_{0}) \to (D \in TotBnd (X) \to \exists t \in (𝒫 ⋃ J \cap Fin) X = ⋃_{y \in t} (y ball (D) (\frac{1}{2^{n}})))$
73	72	ralrimdva	$⊢ D \in CMet (X) \to (D \in TotBnd (X) \to \forall n \in ℕ_{0} \exists t \in (𝒫 ⋃ J \cap Fin) X = ⋃_{y \in t} (y ball (D) (\frac{1}{2^{n}})))$
74	39	pwex	$⊢ 𝒫 ⋃ J \in V$
75	74	inex1	$⊢ 𝒫 ⋃ J \cap Fin \in V$
76		nn0ennn	$⊢ ℕ_{0} \approx ℕ$
77		nnenom	$⊢ ℕ \approx ω$
78	76 77	entri	$⊢ ℕ_{0} \approx ω$
79		iuneq1	$⊢ t = m (n) \to ⋃_{y \in t} (y ball (D) (\frac{1}{2^{n}})) = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}}))$
80	79	eqeq2d	$⊢ t = m (n) \to (X = ⋃_{y \in t} (y ball (D) (\frac{1}{2^{n}})) \leftrightarrow X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}})))$
81	75 78 80	axcc4	$⊢ \forall n \in ℕ_{0} \exists t \in (𝒫 ⋃ J \cap Fin) X = ⋃_{y \in t} (y ball (D) (\frac{1}{2^{n}})) \to \exists m (m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \land \forall n \in ℕ_{0} X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}})))$
82	73 81	syl6	$⊢ D \in CMet (X) \to (D \in TotBnd (X) \to \exists m (m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \land \forall n \in ℕ_{0} X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}}))))$
83		elpwi	$⊢ r \in 𝒫 J \to r \subseteq J$
84		eqid	$⊢ \{u \| \neg \exists v \in (𝒫 r \cap Fin) u \subseteq ⋃ v\} = \{u \| \neg \exists v \in (𝒫 r \cap Fin) u \subseteq ⋃ v\}$
85		eqid	$⊢ \{⟨t, k⟩ \| (k \in ℕ_{0} \land t \in m (k) \land t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) k \in \{u \| \neg \exists v \in (𝒫 r \cap Fin) u \subseteq ⋃ v\})\} = \{⟨t, k⟩ \| (k \in ℕ_{0} \land t \in m (k) \land t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) k \in \{u \| \neg \exists v \in (𝒫 r \cap Fin) u \subseteq ⋃ v\})\}$
86		eqid	$⊢ (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) = (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}}))$
87		simpl	$⊢ (D \in CMet (X) \land (m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \land \forall n \in ℕ_{0} X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}})))) \to D \in CMet (X)$
88	34	pweqd	$⊢ D \in CMet (X) \to 𝒫 X = 𝒫 ⋃ J$
89	88	ineq1d	$⊢ D \in CMet (X) \to 𝒫 X \cap Fin = 𝒫 ⋃ J \cap Fin$
90	89	feq3d	$⊢ D \in CMet (X) \to (m : ℕ_{0} ⟶ 𝒫 X \cap Fin \leftrightarrow m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin)$
91	90	biimpar	$⊢ (D \in CMet (X) \land m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin) \to m : ℕ_{0} ⟶ 𝒫 X \cap Fin$
92	91	adantrr	$⊢ (D \in CMet (X) \land (m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \land \forall n \in ℕ_{0} X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}})))) \to m : ℕ_{0} ⟶ 𝒫 X \cap Fin$
93		oveq1	$⊢ t = y \to t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n = y (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n$
94	93	cbviunv	$⊢ ⋃_{t \in m (n)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n) = ⋃_{y \in m (n)} (y (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n)$
95		id	$⊢ m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \to m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin$
96		inss1	$⊢ 𝒫 ⋃ J \cap Fin \subseteq 𝒫 ⋃ J$
97	96 88	sseqtrrid	$⊢ D \in CMet (X) \to 𝒫 ⋃ J \cap Fin \subseteq 𝒫 X$
98		fss	$⊢ (m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \land 𝒫 ⋃ J \cap Fin \subseteq 𝒫 X) \to m : ℕ_{0} ⟶ 𝒫 X$
99	95 97 98	syl2anr	$⊢ (D \in CMet (X) \land m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin) \to m : ℕ_{0} ⟶ 𝒫 X$
100	99	ffvelrnda	$⊢ ((D \in CMet (X) \land m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin) \land n \in ℕ_{0}) \to m (n) \in 𝒫 X$
101	100	elpwid	$⊢ ((D \in CMet (X) \land m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin) \land n \in ℕ_{0}) \to m (n) \subseteq X$
102	101	sselda	$⊢ (((D \in CMet (X) \land m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin) \land n \in ℕ_{0}) \land y \in m (n)) \to y \in X$
103		simplr	$⊢ (((D \in CMet (X) \land m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin) \land n \in ℕ_{0}) \land y \in m (n)) \to n \in ℕ_{0}$
104		oveq1	$⊢ z = y \to z ball (D) (\frac{1}{2^{m}}) = y ball (D) (\frac{1}{2^{m}})$
105		oveq2	$⊢ m = n \to 2^{m} = 2^{n}$
106	105	oveq2d	$⊢ m = n \to \frac{1}{2^{m}} = \frac{1}{2^{n}}$
107	106	oveq2d	$⊢ m = n \to y ball (D) (\frac{1}{2^{m}}) = y ball (D) (\frac{1}{2^{n}})$
108		ovex	$⊢ y ball (D) (\frac{1}{2^{n}}) \in V$
109	104 107 86 108	ovmpo	$⊢ (y \in X \land n \in ℕ_{0}) \to y (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n = y ball (D) (\frac{1}{2^{n}})$
110	102 103 109	syl2anc	$⊢ (((D \in CMet (X) \land m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin) \land n \in ℕ_{0}) \land y \in m (n)) \to y (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n = y ball (D) (\frac{1}{2^{n}})$
111	110	iuneq2dv	$⊢ ((D \in CMet (X) \land m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin) \land n \in ℕ_{0}) \to ⋃_{y \in m (n)} (y (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n) = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}}))$
112	94 111	eqtrid	$⊢ ((D \in CMet (X) \land m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin) \land n \in ℕ_{0}) \to ⋃_{t \in m (n)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n) = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}}))$
113	112	eqeq2d	$⊢ ((D \in CMet (X) \land m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin) \land n \in ℕ_{0}) \to (X = ⋃_{t \in m (n)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n) \leftrightarrow X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}})))$
114	113	biimprd	$⊢ ((D \in CMet (X) \land m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin) \land n \in ℕ_{0}) \to (X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}})) \to X = ⋃_{t \in m (n)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n))$
115	114	ralimdva	$⊢ (D \in CMet (X) \land m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin) \to (\forall n \in ℕ_{0} X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}})) \to \forall n \in ℕ_{0} X = ⋃_{t \in m (n)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n))$
116	115	impr	$⊢ (D \in CMet (X) \land (m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \land \forall n \in ℕ_{0} X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}})))) \to \forall n \in ℕ_{0} X = ⋃_{t \in m (n)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n)$
117		fveq2	$⊢ n = k \to m (n) = m (k)$
118	117	iuneq1d	$⊢ n = k \to ⋃_{t \in m (n)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n) = ⋃_{t \in m (k)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n)$
119		simpl	$⊢ (n = k \land t \in m (k)) \to n = k$
120	119	oveq2d	$⊢ (n = k \land t \in m (k)) \to t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n = t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) k$
121	120	iuneq2dv	$⊢ n = k \to ⋃_{t \in m (k)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n) = ⋃_{t \in m (k)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) k)$
122	118 121	eqtrd	$⊢ n = k \to ⋃_{t \in m (n)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n) = ⋃_{t \in m (k)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) k)$
123	122	eqeq2d	$⊢ n = k \to (X = ⋃_{t \in m (n)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n) \leftrightarrow X = ⋃_{t \in m (k)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) k))$
124	123	cbvralvw	$⊢ \forall n \in ℕ_{0} X = ⋃_{t \in m (n)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) n) \leftrightarrow \forall k \in ℕ_{0} X = ⋃_{t \in m (k)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) k)$
125	116 124	sylib	$⊢ (D \in CMet (X) \land (m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \land \forall n \in ℕ_{0} X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}})))) \to \forall k \in ℕ_{0} X = ⋃_{t \in m (k)} (t (z \in X, m \in ℕ_{0} ⟼ z ball (D) (\frac{1}{2^{m}})) k)$
126	1 84 85 86 87 92 125	heiborlem10	$⊢ ((D \in CMet (X) \land (m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \land \forall n \in ℕ_{0} X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}})))) \land (r \subseteq J \land ⋃ J = ⋃ r)) \to \exists v \in (𝒫 r \cap Fin) ⋃ J = ⋃ v$
127	126	exp32	$⊢ (D \in CMet (X) \land (m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \land \forall n \in ℕ_{0} X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}})))) \to (r \subseteq J \to (⋃ J = ⋃ r \to \exists v \in (𝒫 r \cap Fin) ⋃ J = ⋃ v))$
128	83 127	syl5	$⊢ (D \in CMet (X) \land (m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \land \forall n \in ℕ_{0} X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}})))) \to (r \in 𝒫 J \to (⋃ J = ⋃ r \to \exists v \in (𝒫 r \cap Fin) ⋃ J = ⋃ v))$
129	128	ralrimiv	$⊢ (D \in CMet (X) \land (m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \land \forall n \in ℕ_{0} X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}})))) \to \forall r \in 𝒫 J (⋃ J = ⋃ r \to \exists v \in (𝒫 r \cap Fin) ⋃ J = ⋃ v)$
130	129	ex	$⊢ D \in CMet (X) \to ((m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \land \forall n \in ℕ_{0} X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}}))) \to \forall r \in 𝒫 J (⋃ J = ⋃ r \to \exists v \in (𝒫 r \cap Fin) ⋃ J = ⋃ v))$
131	130	exlimdv	$⊢ D \in CMet (X) \to (\exists m (m : ℕ_{0} ⟶ 𝒫 ⋃ J \cap Fin \land \forall n \in ℕ_{0} X = ⋃_{y \in m (n)} (y ball (D) (\frac{1}{2^{n}}))) \to \forall r \in 𝒫 J (⋃ J = ⋃ r \to \exists v \in (𝒫 r \cap Fin) ⋃ J = ⋃ v))$
132	82 131	syld	$⊢ D \in CMet (X) \to (D \in TotBnd (X) \to \forall r \in 𝒫 J (⋃ J = ⋃ r \to \exists v \in (𝒫 r \cap Fin) ⋃ J = ⋃ v))$
133	132	imp	$⊢ (D \in CMet (X) \land D \in TotBnd (X)) \to \forall r \in 𝒫 J (⋃ J = ⋃ r \to \exists v \in (𝒫 r \cap Fin) ⋃ J = ⋃ v)$
134		eqid	$⊢ ⋃ J = ⋃ J$
135	134	iscmp	$⊢ J \in Comp \leftrightarrow (J \in Top \land \forall r \in 𝒫 J (⋃ J = ⋃ r \to \exists v \in (𝒫 r \cap Fin) ⋃ J = ⋃ v))$
136	8 133 135	sylanbrc	$⊢ (D \in CMet (X) \land D \in TotBnd (X)) \to J \in Comp$
137	4 136	jca	$⊢ (D \in CMet (X) \land D \in TotBnd (X)) \to (D \in Met (X) \land J \in Comp)$
138	2 137	impbii	$⊢ (D \in Met (X) \land J \in Comp) \leftrightarrow (D \in CMet (X) \land D \in TotBnd (X))$

Metamath Proof Explorer

Theorem heibor

Proof