sstotbnd

Description: Condition for a subset of a metric space to be totally bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

		Ref	Expression
	Hypothesis	sstotbnd.2	$⊢ N = {M ↾}_{(Y \times Y)}$
	Assertion	sstotbnd	$⊢ (M \in Met (X) \land Y \subseteq X) \to (N \in TotBnd (Y) \leftrightarrow \forall d \in ℝ^{+} \exists v \in Fin (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))$

Proof

Step	Hyp	Ref	Expression
1		sstotbnd.2	$⊢ N = {M ↾}_{(Y \times Y)}$
2	1	sstotbnd2	$⊢ (M \in Met (X) \land Y \subseteq X) \to (N \in TotBnd (Y) \leftrightarrow \forall d \in ℝ^{+} \exists u \in (𝒫 X \cap Fin) Y \subseteq ⋃_{x \in u} (x ball (M) d))$
3		elfpw	$⊢ u \in (𝒫 X \cap Fin) \leftrightarrow (u \subseteq X \land u \in Fin)$
4	3	simprbi	$⊢ u \in (𝒫 X \cap Fin) \to u \in Fin$
5		mptfi	$⊢ u \in Fin \to (x \in u ⟼ x ball (M) d) \in Fin$
6		rnfi	$⊢ (x \in u ⟼ x ball (M) d) \in Fin \to ran (x \in u ⟼ x ball (M) d) \in Fin$
7	4 5 6	3syl	$⊢ u \in (𝒫 X \cap Fin) \to ran (x \in u ⟼ x ball (M) d) \in Fin$
8	7	ad2antrl	$⊢ ((M \in Met (X) \land Y \subseteq X) \land (u \in (𝒫 X \cap Fin) \land Y \subseteq ⋃_{x \in u} (x ball (M) d))) \to ran (x \in u ⟼ x ball (M) d) \in Fin$
9		simprr	$⊢ ((M \in Met (X) \land Y \subseteq X) \land (u \in (𝒫 X \cap Fin) \land Y \subseteq ⋃_{x \in u} (x ball (M) d))) \to Y \subseteq ⋃_{x \in u} (x ball (M) d)$
10		eqid	$⊢ (x \in u ⟼ x ball (M) d) = (x \in u ⟼ x ball (M) d)$
11	10	rnmpt	$⊢ ran (x \in u ⟼ x ball (M) d) = \{b \| \exists x \in u b = x ball (M) d\}$
12	3	simplbi	$⊢ u \in (𝒫 X \cap Fin) \to u \subseteq X$
13		ssrexv	$⊢ u \subseteq X \to (\exists x \in u b = x ball (M) d \to \exists x \in X b = x ball (M) d)$
14	12 13	syl	$⊢ u \in (𝒫 X \cap Fin) \to (\exists x \in u b = x ball (M) d \to \exists x \in X b = x ball (M) d)$
15	14	ad2antrl	$⊢ ((M \in Met (X) \land Y \subseteq X) \land (u \in (𝒫 X \cap Fin) \land Y \subseteq ⋃_{x \in u} (x ball (M) d))) \to (\exists x \in u b = x ball (M) d \to \exists x \in X b = x ball (M) d)$
16	15	ss2abdv	$⊢ ((M \in Met (X) \land Y \subseteq X) \land (u \in (𝒫 X \cap Fin) \land Y \subseteq ⋃_{x \in u} (x ball (M) d))) \to \{b \| \exists x \in u b = x ball (M) d\} \subseteq \{b \| \exists x \in X b = x ball (M) d\}$
17	11 16	eqsstrid	$⊢ ((M \in Met (X) \land Y \subseteq X) \land (u \in (𝒫 X \cap Fin) \land Y \subseteq ⋃_{x \in u} (x ball (M) d))) \to ran (x \in u ⟼ x ball (M) d) \subseteq \{b \| \exists x \in X b = x ball (M) d\}$
18		unieq	$⊢ v = ran (x \in u ⟼ x ball (M) d) \to ⋃ v = ⋃ ran (x \in u ⟼ x ball (M) d)$
19		ovex	$⊢ x ball (M) d \in V$
20	19	dfiun3	$⊢ ⋃_{x \in u} (x ball (M) d) = ⋃ ran (x \in u ⟼ x ball (M) d)$
21	18 20	eqtr4di	$⊢ v = ran (x \in u ⟼ x ball (M) d) \to ⋃ v = ⋃_{x \in u} (x ball (M) d)$
22	21	sseq2d	$⊢ v = ran (x \in u ⟼ x ball (M) d) \to (Y \subseteq ⋃ v \leftrightarrow Y \subseteq ⋃_{x \in u} (x ball (M) d))$
23		ssabral	$⊢ v \subseteq \{b \| \exists x \in X b = x ball (M) d\} \leftrightarrow \forall b \in v \exists x \in X b = x ball (M) d$
24		sseq1	$⊢ v = ran (x \in u ⟼ x ball (M) d) \to (v \subseteq \{b \| \exists x \in X b = x ball (M) d\} \leftrightarrow ran (x \in u ⟼ x ball (M) d) \subseteq \{b \| \exists x \in X b = x ball (M) d\})$
25	23 24	bitr3id	$⊢ v = ran (x \in u ⟼ x ball (M) d) \to (\forall b \in v \exists x \in X b = x ball (M) d \leftrightarrow ran (x \in u ⟼ x ball (M) d) \subseteq \{b \| \exists x \in X b = x ball (M) d\})$
26	22 25	anbi12d	$⊢ v = ran (x \in u ⟼ x ball (M) d) \to ((Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d) \leftrightarrow (Y \subseteq ⋃_{x \in u} (x ball (M) d) \land ran (x \in u ⟼ x ball (M) d) \subseteq \{b \| \exists x \in X b = x ball (M) d\}))$
27	26	rspcev	$⊢ (ran (x \in u ⟼ x ball (M) d) \in Fin \land (Y \subseteq ⋃_{x \in u} (x ball (M) d) \land ran (x \in u ⟼ x ball (M) d) \subseteq \{b \| \exists x \in X b = x ball (M) d\})) \to \exists v \in Fin (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d)$
28	8 9 17 27	syl12anc	$⊢ ((M \in Met (X) \land Y \subseteq X) \land (u \in (𝒫 X \cap Fin) \land Y \subseteq ⋃_{x \in u} (x ball (M) d))) \to \exists v \in Fin (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d)$
29	28	rexlimdvaa	$⊢ (M \in Met (X) \land Y \subseteq X) \to (\exists u \in (𝒫 X \cap Fin) Y \subseteq ⋃_{x \in u} (x ball (M) d) \to \exists v \in Fin (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))$
30		oveq1	$⊢ x = f (b) \to x ball (M) d = f (b) ball (M) d$
31	30	eqeq2d	$⊢ x = f (b) \to (b = x ball (M) d \leftrightarrow b = f (b) ball (M) d)$
32	31	ac6sfi	$⊢ (v \in Fin \land \forall b \in v \exists x \in X b = x ball (M) d) \to \exists f (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)$
33	32	adantrl	$⊢ (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d)) \to \exists f (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)$
34	33	adantl	$⊢ ((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \to \exists f (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)$
35		frn	$⊢ f : v ⟶ X \to ran f \subseteq X$
36	35	ad2antrl	$⊢ (((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \land (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)) \to ran f \subseteq X$
37		simplrl	$⊢ (((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \land (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)) \to v \in Fin$
38		ffn	$⊢ f : v ⟶ X \to f Fn v$
39	38	ad2antrl	$⊢ (((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \land (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)) \to f Fn v$
40		dffn4	$⊢ f Fn v \leftrightarrow f : v \underset{onto}{⟶} ran f$
41	39 40	sylib	$⊢ (((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \land (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)) \to f : v \underset{onto}{⟶} ran f$
42		fofi	$⊢ (v \in Fin \land f : v \underset{onto}{⟶} ran f) \to ran f \in Fin$
43	37 41 42	syl2anc	$⊢ (((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \land (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)) \to ran f \in Fin$
44		elfpw	$⊢ ran f \in (𝒫 X \cap Fin) \leftrightarrow (ran f \subseteq X \land ran f \in Fin)$
45	36 43 44	sylanbrc	$⊢ (((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \land (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)) \to ran f \in (𝒫 X \cap Fin)$
46		simprrl	$⊢ ((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \to Y \subseteq ⋃ v$
47	46	adantr	$⊢ (((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \land (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)) \to Y \subseteq ⋃ v$
48		uniiun	$⊢ ⋃ v = ⋃_{b \in v} b$
49		iuneq2	$⊢ \forall b \in v b = f (b) ball (M) d \to ⋃_{b \in v} b = ⋃_{b \in v} (f (b) ball (M) d)$
50	48 49	syl5eq	$⊢ \forall b \in v b = f (b) ball (M) d \to ⋃ v = ⋃_{b \in v} (f (b) ball (M) d)$
51	50	ad2antll	$⊢ (((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \land (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)) \to ⋃ v = ⋃_{b \in v} (f (b) ball (M) d)$
52	47 51	sseqtrd	$⊢ (((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \land (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)) \to Y \subseteq ⋃_{b \in v} (f (b) ball (M) d)$
53	30	eleq2d	$⊢ x = f (b) \to (y \in (x ball (M) d) \leftrightarrow y \in (f (b) ball (M) d))$
54	53	rexrn	$⊢ f Fn v \to (\exists x \in ran f y \in (x ball (M) d) \leftrightarrow \exists b \in v y \in (f (b) ball (M) d))$
55		eliun	$⊢ y \in ⋃_{x \in ran f} (x ball (M) d) \leftrightarrow \exists x \in ran f y \in (x ball (M) d)$
56		eliun	$⊢ y \in ⋃_{b \in v} (f (b) ball (M) d) \leftrightarrow \exists b \in v y \in (f (b) ball (M) d)$
57	54 55 56	3bitr4g	$⊢ f Fn v \to (y \in ⋃_{x \in ran f} (x ball (M) d) \leftrightarrow y \in ⋃_{b \in v} (f (b) ball (M) d))$
58	57	eqrdv	$⊢ f Fn v \to ⋃_{x \in ran f} (x ball (M) d) = ⋃_{b \in v} (f (b) ball (M) d)$
59	39 58	syl	$⊢ (((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \land (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)) \to ⋃_{x \in ran f} (x ball (M) d) = ⋃_{b \in v} (f (b) ball (M) d)$
60	52 59	sseqtrrd	$⊢ (((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \land (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)) \to Y \subseteq ⋃_{x \in ran f} (x ball (M) d)$
61		iuneq1	$⊢ u = ran f \to ⋃_{x \in u} (x ball (M) d) = ⋃_{x \in ran f} (x ball (M) d)$
62	61	sseq2d	$⊢ u = ran f \to (Y \subseteq ⋃_{x \in u} (x ball (M) d) \leftrightarrow Y \subseteq ⋃_{x \in ran f} (x ball (M) d))$
63	62	rspcev	$⊢ (ran f \in (𝒫 X \cap Fin) \land Y \subseteq ⋃_{x \in ran f} (x ball (M) d)) \to \exists u \in (𝒫 X \cap Fin) Y \subseteq ⋃_{x \in u} (x ball (M) d)$
64	45 60 63	syl2anc	$⊢ (((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \land (f : v ⟶ X \land \forall b \in v b = f (b) ball (M) d)) \to \exists u \in (𝒫 X \cap Fin) Y \subseteq ⋃_{x \in u} (x ball (M) d)$
65	34 64	exlimddv	$⊢ ((M \in Met (X) \land Y \subseteq X) \land (v \in Fin \land (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))) \to \exists u \in (𝒫 X \cap Fin) Y \subseteq ⋃_{x \in u} (x ball (M) d)$
66	65	rexlimdvaa	$⊢ (M \in Met (X) \land Y \subseteq X) \to (\exists v \in Fin (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d) \to \exists u \in (𝒫 X \cap Fin) Y \subseteq ⋃_{x \in u} (x ball (M) d))$
67	29 66	impbid	$⊢ (M \in Met (X) \land Y \subseteq X) \to (\exists u \in (𝒫 X \cap Fin) Y \subseteq ⋃_{x \in u} (x ball (M) d) \leftrightarrow \exists v \in Fin (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))$
68	67	ralbidv	$⊢ (M \in Met (X) \land Y \subseteq X) \to (\forall d \in ℝ^{+} \exists u \in (𝒫 X \cap Fin) Y \subseteq ⋃_{x \in u} (x ball (M) d) \leftrightarrow \forall d \in ℝ^{+} \exists v \in Fin (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))$
69	2 68	bitrd	$⊢ (M \in Met (X) \land Y \subseteq X) \to (N \in TotBnd (Y) \leftrightarrow \forall d \in ℝ^{+} \exists v \in Fin (Y \subseteq ⋃ v \land \forall b \in v \exists x \in X b = x ball (M) d))$

Metamath Proof Explorer

Theorem sstotbnd

Proof