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 ‘ 𝐷 ) 𝑑 ) ⊆ 𝑢 )