Metamath Proof Explorer

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 ‘ 𝑀 ) 𝑟 ) ) )