Metamath Proof Explorer


Theorem xlebnum

Description: Generalize lebnum to extended metrics. (Contributed by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypotheses xlebnum.j 𝐽 = ( MetOpen ‘ 𝐷 )
xlebnum.d ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
xlebnum.c ( 𝜑𝐽 ∈ Comp )
xlebnum.s ( 𝜑𝑈𝐽 )
xlebnum.u ( 𝜑𝑋 = 𝑈 )
Assertion xlebnum ( 𝜑 → ∃ 𝑑 ∈ ℝ+𝑥𝑋𝑢𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )

Proof

Step Hyp Ref Expression
1 xlebnum.j 𝐽 = ( MetOpen ‘ 𝐷 )
2 xlebnum.d ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3 xlebnum.c ( 𝜑𝐽 ∈ Comp )
4 xlebnum.s ( 𝜑𝑈𝐽 )
5 xlebnum.u ( 𝜑𝑋 = 𝑈 )
6 eqid ( MetOpen ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) = ( MetOpen ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) )
7 1rp 1 ∈ ℝ+
8 eqid ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) = ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) )
9 8 stdbdmet ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 1 ∈ ℝ+ ) → ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ∈ ( Met ‘ 𝑋 ) )
10 2 7 9 sylancl ( 𝜑 → ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ∈ ( Met ‘ 𝑋 ) )
11 rpxr ( 1 ∈ ℝ+ → 1 ∈ ℝ* )
12 7 11 mp1i ( 𝜑 → 1 ∈ ℝ* )
13 0lt1 0 < 1
14 13 a1i ( 𝜑 → 0 < 1 )
15 8 1 stdbdmopn ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 1 ∈ ℝ* ∧ 0 < 1 ) → 𝐽 = ( MetOpen ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) )
16 2 12 14 15 syl3anc ( 𝜑𝐽 = ( MetOpen ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) )
17 16 3 eqeltrrd ( 𝜑 → ( MetOpen ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) ∈ Comp )
18 4 16 sseqtrd ( 𝜑𝑈 ⊆ ( MetOpen ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) )
19 6 10 17 18 5 lebnum ( 𝜑 → ∃ 𝑟 ∈ ℝ+𝑥𝑋𝑢𝑈 ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) 𝑟 ) ⊆ 𝑢 )
20 simpr ( ( 𝜑𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
21 ifcl ( ( 𝑟 ∈ ℝ+ ∧ 1 ∈ ℝ+ ) → if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ∈ ℝ+ )
22 20 7 21 sylancl ( ( 𝜑𝑟 ∈ ℝ+ ) → if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ∈ ℝ+ )
23 2 ad2antrr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
24 7 11 mp1i ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → 1 ∈ ℝ* )
25 13 a1i ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → 0 < 1 )
26 simpr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → 𝑥𝑋 )
27 22 adantr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ∈ ℝ+ )
28 rpxr ( if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ∈ ℝ+ → if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ∈ ℝ* )
29 27 28 syl ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ∈ ℝ* )
30 rpre ( 𝑟 ∈ ℝ+𝑟 ∈ ℝ )
31 30 ad2antlr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → 𝑟 ∈ ℝ )
32 1re 1 ∈ ℝ
33 min2 ( ( 𝑟 ∈ ℝ ∧ 1 ∈ ℝ ) → if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ≤ 1 )
34 31 32 33 sylancl ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ≤ 1 )
35 8 stdbdbl ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 1 ∈ ℝ* ∧ 0 < 1 ) ∧ ( 𝑥𝑋 ∧ if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ∈ ℝ* ∧ if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ≤ 1 ) ) → ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) = ( 𝑥 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) )
36 23 24 25 26 29 34 35 syl33anc ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) = ( 𝑥 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) )
37 10 ad2antrr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ∈ ( Met ‘ 𝑋 ) )
38 metxmet ( ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ∈ ( Met ‘ 𝑋 ) → ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ∈ ( ∞Met ‘ 𝑋 ) )
39 37 38 syl ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ∈ ( ∞Met ‘ 𝑋 ) )
40 rpxr ( 𝑟 ∈ ℝ+𝑟 ∈ ℝ* )
41 40 ad2antlr ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → 𝑟 ∈ ℝ* )
42 min1 ( ( 𝑟 ∈ ℝ ∧ 1 ∈ ℝ ) → if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ≤ 𝑟 )
43 31 32 42 sylancl ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ≤ 𝑟 )
44 ssbl ( ( ( ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥𝑋 ) ∧ ( if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ∈ ℝ*𝑟 ∈ ℝ* ) ∧ if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ≤ 𝑟 ) → ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) ⊆ ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) 𝑟 ) )
45 39 26 29 41 43 44 syl221anc ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) ⊆ ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) 𝑟 ) )
46 36 45 eqsstrrd ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → ( 𝑥 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) ⊆ ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) 𝑟 ) )
47 sstr2 ( ( 𝑥 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) ⊆ ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) 𝑟 ) → ( ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) 𝑟 ) ⊆ 𝑢 → ( 𝑥 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) ⊆ 𝑢 ) )
48 46 47 syl ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → ( ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) 𝑟 ) ⊆ 𝑢 → ( 𝑥 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) ⊆ 𝑢 ) )
49 48 reximdv ( ( ( 𝜑𝑟 ∈ ℝ+ ) ∧ 𝑥𝑋 ) → ( ∃ 𝑢𝑈 ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) 𝑟 ) ⊆ 𝑢 → ∃ 𝑢𝑈 ( 𝑥 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) ⊆ 𝑢 ) )
50 49 ralimdva ( ( 𝜑𝑟 ∈ ℝ+ ) → ( ∀ 𝑥𝑋𝑢𝑈 ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) 𝑟 ) ⊆ 𝑢 → ∀ 𝑥𝑋𝑢𝑈 ( 𝑥 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) ⊆ 𝑢 ) )
51 oveq2 ( 𝑑 = if ( 𝑟 ≤ 1 , 𝑟 , 1 ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) = ( 𝑥 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) )
52 51 sseq1d ( 𝑑 = if ( 𝑟 ≤ 1 , 𝑟 , 1 ) → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ↔ ( 𝑥 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) ⊆ 𝑢 ) )
53 52 rexbidv ( 𝑑 = if ( 𝑟 ≤ 1 , 𝑟 , 1 ) → ( ∃ 𝑢𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ↔ ∃ 𝑢𝑈 ( 𝑥 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) ⊆ 𝑢 ) )
54 53 ralbidv ( 𝑑 = if ( 𝑟 ≤ 1 , 𝑟 , 1 ) → ( ∀ 𝑥𝑋𝑢𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ↔ ∀ 𝑥𝑋𝑢𝑈 ( 𝑥 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) ⊆ 𝑢 ) )
55 54 rspcev ( ( if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ∈ ℝ+ ∧ ∀ 𝑥𝑋𝑢𝑈 ( 𝑥 ( ball ‘ 𝐷 ) if ( 𝑟 ≤ 1 , 𝑟 , 1 ) ) ⊆ 𝑢 ) → ∃ 𝑑 ∈ ℝ+𝑥𝑋𝑢𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )
56 22 50 55 syl6an ( ( 𝜑𝑟 ∈ ℝ+ ) → ( ∀ 𝑥𝑋𝑢𝑈 ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) 𝑟 ) ⊆ 𝑢 → ∃ 𝑑 ∈ ℝ+𝑥𝑋𝑢𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) )
57 56 rexlimdva ( 𝜑 → ( ∃ 𝑟 ∈ ℝ+𝑥𝑋𝑢𝑈 ( 𝑥 ( ball ‘ ( 𝑦𝑋 , 𝑧𝑋 ↦ if ( ( 𝑦 𝐷 𝑧 ) ≤ 1 , ( 𝑦 𝐷 𝑧 ) , 1 ) ) ) 𝑟 ) ⊆ 𝑢 → ∃ 𝑑 ∈ ℝ+𝑥𝑋𝑢𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 ) )
58 19 57 mpd ( 𝜑 → ∃ 𝑑 ∈ ℝ+𝑥𝑋𝑢𝑈 ( 𝑥 ( ball ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )