Theorem isbndx

Description: A "bounded extended metric" (meaning that it satisfies the same condition as a bounded metric, but with "metric" replaced with "extended metric") is a metric and thus is bounded in the conventional sense. (Contributed by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Assertion	isbndx	⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isbnd	⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
2		metxmet	⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
3		simpr	⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) )
4		xmetf	⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
5		ffn	⊢ ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → 𝑀 Fn ( 𝑋 × 𝑋 ) )
6	3 4 5	3syl	⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ) → 𝑀 Fn ( 𝑋 × 𝑋 ) )
7		simprr	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ) → 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) )
8		rpxr	⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
9		eqid	⊢ ( ◡ 𝑀 “ ℝ ) = ( ◡ 𝑀 “ ℝ )
10	9	blssec	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ⊆ [ 𝑥 ] ( ◡ 𝑀 “ ℝ ) )
11	10	3expa	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ⊆ [ 𝑥 ] ( ◡ 𝑀 “ ℝ ) )
12	8 11	sylan2	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ⊆ [ 𝑥 ] ( ◡ 𝑀 “ ℝ ) )
13	12	adantrr	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ) → ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ⊆ [ 𝑥 ] ( ◡ 𝑀 “ ℝ ) )
14	7 13	eqsstrd	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ) → 𝑋 ⊆ [ 𝑥 ] ( ◡ 𝑀 “ ℝ ) )
15	14	sselda	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ [ 𝑥 ] ( ◡ 𝑀 “ ℝ ) )
16		vex	⊢ 𝑦 ∈ V
17		vex	⊢ 𝑥 ∈ V
18	16 17	elec	⊢ ( 𝑦 ∈ [ 𝑥 ] ( ◡ 𝑀 “ ℝ ) ↔ 𝑥 ( ◡ 𝑀 “ ℝ ) 𝑦 )
19	15 18	sylib	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ 𝑦 ∈ 𝑋 ) → 𝑥 ( ◡ 𝑀 “ ℝ ) 𝑦 )
20	9	xmeterval	⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ( ◡ 𝑀 “ ℝ ) 𝑦 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝑥 𝑀 𝑦 ) ∈ ℝ ) ) )
21	20	ad3antrrr	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( ◡ 𝑀 “ ℝ ) 𝑦 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝑥 𝑀 𝑦 ) ∈ ℝ ) ) )
22	19 21	mpbid	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝑥 𝑀 𝑦 ) ∈ ℝ ) )
23	22	simp3d	⊢ ( ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑀 𝑦 ) ∈ ℝ )
24	23	ralrimiva	⊢ ( ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ+ ∧ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ) → ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) ∈ ℝ )
25	24	rexlimdvaa	⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) ∈ ℝ ) )
26	25	ralimdva	⊢ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) ∈ ℝ ) )
27	26	impcom	⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) ∈ ℝ )
28		ffnov	⊢ ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ ↔ ( 𝑀 Fn ( 𝑋 × 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑀 𝑦 ) ∈ ℝ ) )
29	6 27 28	sylanbrc	⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ) → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ )
30		ismet2	⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 : ( 𝑋 × 𝑋 ) ⟶ ℝ ) )
31	3 29 30	sylanbrc	⊢ ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ∧ 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
32	31	ex	⊢ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) → 𝑀 ∈ ( Met ‘ 𝑋 ) ) )
33	2 32	impbid2	⊢ ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) → ( 𝑀 ∈ ( Met ‘ 𝑋 ) ↔ 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ) )
34	33	pm5.32ri	⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )
35	1 34	bitri	⊢ ( 𝑀 ∈ ( Bnd ‘ 𝑋 ) ↔ ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ ℝ+ 𝑋 = ( 𝑥 ( ball ‘ 𝑀 ) 𝑟 ) ) )