equivtotbnd

Description: If the metric M is "strongly finer" than N (meaning that there is a positive real constant R such that N ( x , y ) <_ R x. M ( x , y ) ), then total boundedness of M implies total boundedness of N . (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then one is totally bounded iff the other is.) (Contributed by Mario Carneiro, 14-Sep-2015)

	Ref	Expression
Hypotheses	equivtotbnd.1	⊢ ( 𝜑 → 𝑀 ∈ ( TotBnd ‘ 𝑋 ) )
	equivtotbnd.2	⊢ ( 𝜑 → 𝑁 ∈ ( Met ‘ 𝑋 ) )
	equivtotbnd.3	⊢ ( 𝜑 → 𝑅 ∈ ℝ⁺ )
	equivtotbnd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) )
Assertion	equivtotbnd	⊢ ( 𝜑 → 𝑁 ∈ ( TotBnd ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		equivtotbnd.1	⊢ ( 𝜑 → 𝑀 ∈ ( TotBnd ‘ 𝑋 ) )
2		equivtotbnd.2	⊢ ( 𝜑 → 𝑁 ∈ ( Met ‘ 𝑋 ) )
3		equivtotbnd.3	⊢ ( 𝜑 → 𝑅 ∈ ℝ⁺ )
4		equivtotbnd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) )
5		simpr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) → 𝑟 ∈ ℝ⁺ )
6	3	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) → 𝑅 ∈ ℝ⁺ )
7	5 6	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) → ( 𝑟 / 𝑅 ) ∈ ℝ⁺ )
8	1	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) → 𝑀 ∈ ( TotBnd ‘ 𝑋 ) )
9		istotbnd3	⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ ℝ⁺ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = 𝑋 ) )
10	9	simprbi	⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) → ∀ 𝑠 ∈ ℝ⁺ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = 𝑋 )
11	8 10	syl	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) → ∀ 𝑠 ∈ ℝ⁺ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = 𝑋 )
12		oveq2	⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) )
13	12	iuneq2d	⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) )
14	13	eqeq1d	⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = 𝑋 ↔ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 ) )
15	14	rexbidv	⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = 𝑋 ↔ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 ) )
16	15	rspcv	⊢ ( ( 𝑟 / 𝑅 ) ∈ ℝ⁺ → ( ∀ 𝑠 ∈ ℝ⁺ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) 𝑠 ) = 𝑋 → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 ) )
17	7 11 16	sylc	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 )
18		elfpw	⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ↔ ( 𝑣 ⊆ 𝑋 ∧ 𝑣 ∈ Fin ) )
19	18	simplbi	⊢ ( 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) → 𝑣 ⊆ 𝑋 )
20	19	adantl	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → 𝑣 ⊆ 𝑋 )
21	20	sselda	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑥 ∈ 𝑋 )
22		eqid	⊢ ( MetOpen ‘ 𝑁 ) = ( MetOpen ‘ 𝑁 )
23		eqid	⊢ ( MetOpen ‘ 𝑀 ) = ( MetOpen ‘ 𝑀 )
24	9	simplbi	⊢ ( 𝑀 ∈ ( TotBnd ‘ 𝑋 ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
25	1 24	syl	⊢ ( 𝜑 → 𝑀 ∈ ( Met ‘ 𝑋 ) )
26	22 23 2 25 3 4	metss2lem	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
27	26	anass1rs	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
28	27	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
29	21 28	syldan	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
30	29	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ∀ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
31		ss2iun	⊢ ( ∀ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
32	30 31	syl	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) )
33		sseq1	⊢ ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ↔ 𝑋 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ) )
34	32 33	syl5ibcom	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 → 𝑋 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ) )
35	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑁 ∈ ( Met ‘ 𝑋 ) )
36		metxmet	⊢ ( 𝑁 ∈ ( Met ‘ 𝑋 ) → 𝑁 ∈ ( ∞Met ‘ 𝑋 ) )
37	35 36	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑁 ∈ ( ∞Met ‘ 𝑋 ) )
38		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑟 ∈ ℝ⁺ )
39	38	rpxrd	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → 𝑟 ∈ ℝ^* )
40		blssm	⊢ ( ( 𝑁 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ^* ) → ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 )
41	37 21 39 40	syl3anc	⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) ∧ 𝑥 ∈ 𝑣 ) → ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 )
42	41	ralrimiva	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ∀ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 )
43		iunss	⊢ ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 ↔ ∀ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 )
44	42 43	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 )
45	34 44	jctild	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ) ) )
46		eqss	⊢ ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) = 𝑋 ↔ ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ⊆ 𝑋 ∧ 𝑋 ⊆ ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) ) )
47	45 46	imbitrrdi	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) ∧ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ) → ( ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 → ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) = 𝑋 ) )
48	47	reximdva	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑀 ) ( 𝑟 / 𝑅 ) ) = 𝑋 → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) = 𝑋 ) )
49	17 48	mpd	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ⁺ ) → ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) = 𝑋 )
50	49	ralrimiva	⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) = 𝑋 )
51		istotbnd3	⊢ ( 𝑁 ∈ ( TotBnd ‘ 𝑋 ) ↔ ( 𝑁 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑣 ∈ ( 𝒫 𝑋 ∩ Fin ) ∪ 𝑥 ∈ 𝑣 ( 𝑥 ( ball ‘ 𝑁 ) 𝑟 ) = 𝑋 ) )
52	2 50 51	sylanbrc	⊢ ( 𝜑 → 𝑁 ∈ ( TotBnd ‘ 𝑋 ) )

Metamath Proof Explorer

Theorem equivtotbnd

Proof