Metamath Proof Explorer

Theorem stdbdmopn

Description: The standard bounded metric corresponding to C generates the same topology as C . (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses stdbdmet.1 ⊢ 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) )
stdbdmopn.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
Assertion stdbdmopn ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) → 𝐽 = ( MetOpen ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 stdbdmet.1 ⊢ 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) )
2 stdbdmopn.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
3 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
4 3 ad2antll ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ* )
5 simpl2 ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑅 ∈ ℝ* )
6 4 5 ifcld ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ∈ ℝ* )
7 rpre ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
8 7 ad2antll ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ )
9 rpgt0 ⊢ ( 𝑟 ∈ ℝ+ → 0 < 𝑟 )
10 9 ad2antll ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → 0 < 𝑟 )
11 simpl3 ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → 0 < 𝑅 )
12 breq2 ⊢ ( 𝑟 = if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) → ( 0 < 𝑟 ↔ 0 < if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) )
13 breq2 ⊢ ( 𝑅 = if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) → ( 0 < 𝑅 ↔ 0 < if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) )
14 12 13 ifboth ⊢ ( ( 0 < 𝑟 ∧ 0 < 𝑅 ) → 0 < if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) )
15 10 11 14 syl2anc ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → 0 < if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) )
16 0xr ⊢ 0 ∈ ℝ*
17 xrltle ⊢ ( ( 0 ∈ ℝ* ∧ if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ∈ ℝ* ) → ( 0 < if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) → 0 ≤ if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) )
18 16 6 17 sylancr ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ( 0 < if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) → 0 ≤ if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) )
19 15 18 mpd ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → 0 ≤ if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) )
20 xrmin1 ⊢ ( ( 𝑟 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ) → if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ≤ 𝑟 )
21 4 5 20 syl2anc ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ≤ 𝑟 )
22 xrrege0 ⊢ ( ( ( if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ∈ ℝ* ∧ 𝑟 ∈ ℝ ) ∧ ( 0 ≤ if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ∧ if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ≤ 𝑟 ) ) → if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ∈ ℝ )
23 6 8 19 21 22 syl22anc ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ∈ ℝ )
24 23 15 elrpd ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ∈ ℝ+ )
25 simprl ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑧 ∈ 𝑋 )
26 xrmin2 ⊢ ( ( 𝑟 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ) → if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ≤ 𝑅 )
27 4 5 26 syl2anc ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ≤ 𝑅 )
28 25 6 27 3jca ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑧 ∈ 𝑋 ∧ if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ∈ ℝ* ∧ if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ≤ 𝑅 ) )
29 1 stdbdbl ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ∈ ℝ* ∧ if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ≤ 𝑅 ) ) → ( 𝑧 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) = ( 𝑧 ( ball ‘ 𝐶 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) )
30 28 29 syldan ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑧 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) = ( 𝑧 ( ball ‘ 𝐶 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) )
31 30 eqcomd ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑧 ( ball ‘ 𝐶 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) = ( 𝑧 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) )
32 breq1 ⊢ ( 𝑠 = if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) → ( 𝑠 ≤ 𝑟 ↔ if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ≤ 𝑟 ) )
33 oveq2 ⊢ ( 𝑠 = if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) → ( 𝑧 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑧 ( ball ‘ 𝐶 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) )
34 oveq2 ⊢ ( 𝑠 = if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) → ( 𝑧 ( ball ‘ 𝐷 ) 𝑠 ) = ( 𝑧 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) )
35 33 34 eqeq12d ⊢ ( 𝑠 = if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) → ( ( 𝑧 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑧 ( ball ‘ 𝐷 ) 𝑠 ) ↔ ( 𝑧 ( ball ‘ 𝐶 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) = ( 𝑧 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) ) )
36 32 35 anbi12d ⊢ ( 𝑠 = if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) → ( ( 𝑠 ≤ 𝑟 ∧ ( 𝑧 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑧 ( ball ‘ 𝐷 ) 𝑠 ) ) ↔ ( if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ≤ 𝑟 ∧ ( 𝑧 ( ball ‘ 𝐶 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) = ( 𝑧 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) ) ) )
37 36 rspcev ⊢ ( ( if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ∈ ℝ+ ∧ ( if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ≤ 𝑟 ∧ ( 𝑧 ( ball ‘ 𝐶 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) = ( 𝑧 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 𝑅 , 𝑟 , 𝑅 ) ) ) ) → ∃ 𝑠 ∈ ℝ+ ( 𝑠 ≤ 𝑟 ∧ ( 𝑧 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑧 ( ball ‘ 𝐷 ) 𝑠 ) ) )
38 24 21 31 37 syl12anc ⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ∃ 𝑠 ∈ ℝ+ ( 𝑠 ≤ 𝑟 ∧ ( 𝑧 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑧 ( ball ‘ 𝐷 ) 𝑠 ) ) )
39 38 ralrimivva ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑠 ≤ 𝑟 ∧ ( 𝑧 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑧 ( ball ‘ 𝐷 ) 𝑠 ) ) )
40 simp1 ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
41 1 stdbdxmet ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
42 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
43 2 42 metequiv2 ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( ∀ 𝑧 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑠 ≤ 𝑟 ∧ ( 𝑧 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑧 ( ball ‘ 𝐷 ) 𝑠 ) ) → 𝐽 = ( MetOpen ‘ 𝐷 ) ) )
44 40 41 43 syl2anc ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) → ( ∀ 𝑧 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑠 ≤ 𝑟 ∧ ( 𝑧 ( ball ‘ 𝐶 ) 𝑠 ) = ( 𝑧 ( ball ‘ 𝐷 ) 𝑠 ) ) → 𝐽 = ( MetOpen ‘ 𝐷 ) ) )
45 39 44 mpd ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅 ) → 𝐽 = ( MetOpen ‘ 𝐷 ) )