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 β€˜ 𝐷 ) )