isbnd2

Description: The predicate "is a bounded metric space". Uses a single point instead of an arbitrary point in the space. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	isbnd2	⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 ≠ ∅ ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isbndx	⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
2	1	anbi1i	⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 ≠ ∅ ) ↔ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ∧ 𝑋 ≠ ∅ ) )
3		anass	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ∧ 𝑋 ≠ ∅ ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑋 ≠ ∅ ) ) )
4		r19.2z	⊢ ( ( 𝑋 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
5	4	ancoms	⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑋 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
6		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) )
7	6	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ↔ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ) )
8		oveq2	⊢ ( 𝑟 = 𝑠 → ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) )
9	8	eqeq2d	⊢ ( 𝑟 = 𝑠 → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑟 ) ↔ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) )
10	7 9	cbvrex2vw	⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ↔ ∃ 𝑦 ∈ 𝑋 ∃ 𝑠 ∈ ℝ⁺ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) )
11		2rp	⊢ 2 ∈ ℝ⁺
12		rpmulcl	⊢ ( ( 2 ∈ ℝ⁺ ∧ 𝑠 ∈ ℝ⁺ ) → ( 2 · 𝑠 ) ∈ ℝ⁺ )
13	11 12	mpan	⊢ ( 𝑠 ∈ ℝ⁺ → ( 2 · 𝑠 ) ∈ ℝ⁺ )
14	13	ad2antll	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) → ( 2 · 𝑠 ) ∈ ℝ⁺ )
15	14	ad2antrr	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) → ( 2 · 𝑠 ) ∈ ℝ⁺ )
16		rpcn	⊢ ( 𝑠 ∈ ℝ⁺ → 𝑠 ∈ ℂ )
17		2cnd	⊢ ( 𝑠 ∈ ℝ⁺ → 2 ∈ ℂ )
18		2ne0	⊢ 2 ≠ 0
19	18	a1i	⊢ ( 𝑠 ∈ ℝ⁺ → 2 ≠ 0 )
20		divcan3	⊢ ( ( 𝑠 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · 𝑠 ) / 2 ) = 𝑠 )
21	20	eqcomd	⊢ ( ( 𝑠 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → 𝑠 = ( ( 2 · 𝑠 ) / 2 ) )
22	16 17 19 21	syl3anc	⊢ ( 𝑠 ∈ ℝ⁺ → 𝑠 = ( ( 2 · 𝑠 ) / 2 ) )
23	22	oveq2d	⊢ ( 𝑠 ∈ ℝ⁺ → ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) )
24	23	eqeq2d	⊢ ( 𝑠 ∈ ℝ⁺ → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ↔ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) )
25	24	biimpd	⊢ ( 𝑠 ∈ ℝ⁺ → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) → 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) )
26	25	ad2antll	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) → 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) )
27	26	adantr	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) → 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) )
28	27	imp	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) → 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) )
29		simpr	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) → 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) )
30		eleq2	⊢ ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) → ( 𝑥 ∈ 𝑋 ↔ 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) )
31	30	biimpac	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) → 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) )
32		2re	⊢ 2 ∈ ℝ
33		rpre	⊢ ( 𝑠 ∈ ℝ⁺ → 𝑠 ∈ ℝ )
34		remulcl	⊢ ( ( 2 ∈ ℝ ∧ 𝑠 ∈ ℝ ) → ( 2 · 𝑠 ) ∈ ℝ )
35	32 33 34	sylancr	⊢ ( 𝑠 ∈ ℝ⁺ → ( 2 · 𝑠 ) ∈ ℝ )
36		blhalf	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( ( 2 · 𝑠 ) ∈ ℝ ∧ 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
37	36	expr	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( 2 · 𝑠 ) ∈ ℝ ) → ( 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ) )
38	35 37	sylan2	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑠 ∈ ℝ⁺ ) → ( 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ) )
39	38	anasss	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) → ( 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ) )
40	39	imp	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ 𝑥 ∈ ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
41	31 40	sylan2	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
42	41	anassrs	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) → ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
43	29 42	eqsstrd	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) ( ( 2 · 𝑠 ) / 2 ) ) ) → 𝑋 ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
44	28 43	syldan	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) → 𝑋 ⊆ ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
45	13	adantl	⊢ ( ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) → ( 2 · 𝑠 ) ∈ ℝ⁺ )
46		rpxr	⊢ ( ( 2 · 𝑠 ) ∈ ℝ⁺ → ( 2 · 𝑠 ) ∈ ℝ^* )
47		blssm	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 2 · 𝑠 ) ∈ ℝ^* ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ⊆ 𝑋 )
48	46 47	syl3an3	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 2 · 𝑠 ) ∈ ℝ⁺ ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ⊆ 𝑋 )
49	48	3expa	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 2 · 𝑠 ) ∈ ℝ⁺ ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ⊆ 𝑋 )
50	45 49	sylan2	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ⊆ 𝑋 )
51	50	an32s	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ⊆ 𝑋 )
52	51	adantr	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) → ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ⊆ 𝑋 )
53	44 52	eqssd	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) → 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
54		oveq2	⊢ ( 𝑟 = ( 2 · 𝑠 ) → ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) = ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) )
55	54	rspceeqv	⊢ ( ( ( 2 · 𝑠 ) ∈ ℝ⁺ ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) ( 2 · 𝑠 ) ) ) → ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
56	15 53 55	syl2anc	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) ) → ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
57	56	ex	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) → ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
58	57	ralrimdva	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑠 ∈ ℝ⁺ ) ) → ( 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
59	58	rexlimdvva	⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( ∃ 𝑦 ∈ 𝑋 ∃ 𝑠 ∈ ℝ⁺ 𝑋 = ( 𝑦 ( ball ‘ 𝑀 ) 𝑠 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
60	10 59	biimtrid	⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
61		rexn0	⊢ ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → 𝑋 ≠ ∅ )
62	61	a1i	⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → 𝑋 ≠ ∅ ) )
63	60 62	jcad	⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑋 ≠ ∅ ) ) )
64	5 63	impbid2	⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑋 ≠ ∅ ) ↔ ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
65	64	pm5.32i	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑋 ≠ ∅ ) ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
66	2 3 65	3bitri	⊢ ( ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ∧ 𝑋 ≠ ∅ ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∃ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ⁺ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )

Metamath Proof Explorer

Theorem isbnd2

Proof