Metamath Proof Explorer


Theorem metss2lem

Description: Lemma for metss2 . (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypotheses metequiv.3 𝐽 = ( MetOpen ‘ 𝐶 )
metequiv.4 𝐾 = ( MetOpen ‘ 𝐷 )
metss2.1 ( 𝜑𝐶 ∈ ( Met ‘ 𝑋 ) )
metss2.2 ( 𝜑𝐷 ∈ ( Met ‘ 𝑋 ) )
metss2.3 ( 𝜑𝑅 ∈ ℝ+ )
metss2.4 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
Assertion metss2lem ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑆 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑆 ) )

Proof

Step Hyp Ref Expression
1 metequiv.3 𝐽 = ( MetOpen ‘ 𝐶 )
2 metequiv.4 𝐾 = ( MetOpen ‘ 𝐷 )
3 metss2.1 ( 𝜑𝐶 ∈ ( Met ‘ 𝑋 ) )
4 metss2.2 ( 𝜑𝐷 ∈ ( Met ‘ 𝑋 ) )
5 metss2.3 ( 𝜑𝑅 ∈ ℝ+ )
6 metss2.4 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
7 4 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
8 simplrl ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → 𝑥𝑋 )
9 simpr ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → 𝑦𝑋 )
10 metcl ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥𝑋𝑦𝑋 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
11 7 8 9 10 syl3anc ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
12 simplrr ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → 𝑆 ∈ ℝ+ )
13 12 rpred ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → 𝑆 ∈ ℝ )
14 5 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → 𝑅 ∈ ℝ+ )
15 11 13 14 ltmuldiv2d ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → ( ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) < 𝑆 ↔ ( 𝑥 𝐷 𝑦 ) < ( 𝑆 / 𝑅 ) ) )
16 6 anassrs ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑦𝑋 ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
17 16 adantlrr ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) )
18 3 ad2antrr ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → 𝐶 ∈ ( Met ‘ 𝑋 ) )
19 metcl ( ( 𝐶 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥𝑋𝑦𝑋 ) → ( 𝑥 𝐶 𝑦 ) ∈ ℝ )
20 18 8 9 19 syl3anc ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → ( 𝑥 𝐶 𝑦 ) ∈ ℝ )
21 14 rpred ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → 𝑅 ∈ ℝ )
22 21 11 remulcld ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) ∈ ℝ )
23 lelttr ( ( ( 𝑥 𝐶 𝑦 ) ∈ ℝ ∧ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) ∈ ℝ ∧ 𝑆 ∈ ℝ ) → ( ( ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) ∧ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) < 𝑆 ) → ( 𝑥 𝐶 𝑦 ) < 𝑆 ) )
24 20 22 13 23 syl3anc ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → ( ( ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) ∧ ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) < 𝑆 ) → ( 𝑥 𝐶 𝑦 ) < 𝑆 ) )
25 17 24 mpand ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → ( ( 𝑅 · ( 𝑥 𝐷 𝑦 ) ) < 𝑆 → ( 𝑥 𝐶 𝑦 ) < 𝑆 ) )
26 15 25 sylbird ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) ∧ 𝑦𝑋 ) → ( ( 𝑥 𝐷 𝑦 ) < ( 𝑆 / 𝑅 ) → ( 𝑥 𝐶 𝑦 ) < 𝑆 ) )
27 26 ss2rabdv ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) → { 𝑦𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < ( 𝑆 / 𝑅 ) } ⊆ { 𝑦𝑋 ∣ ( 𝑥 𝐶 𝑦 ) < 𝑆 } )
28 metxmet ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
29 4 28 syl ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
30 29 adantr ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
31 simprl ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) → 𝑥𝑋 )
32 simpr ( ( 𝑥𝑋𝑆 ∈ ℝ+ ) → 𝑆 ∈ ℝ+ )
33 rpdivcl ( ( 𝑆 ∈ ℝ+𝑅 ∈ ℝ+ ) → ( 𝑆 / 𝑅 ) ∈ ℝ+ )
34 32 5 33 syl2anr ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) → ( 𝑆 / 𝑅 ) ∈ ℝ+ )
35 34 rpxrd ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) → ( 𝑆 / 𝑅 ) ∈ ℝ* )
36 blval ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥𝑋 ∧ ( 𝑆 / 𝑅 ) ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑆 / 𝑅 ) ) = { 𝑦𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < ( 𝑆 / 𝑅 ) } )
37 30 31 35 36 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑆 / 𝑅 ) ) = { 𝑦𝑋 ∣ ( 𝑥 𝐷 𝑦 ) < ( 𝑆 / 𝑅 ) } )
38 metxmet ( 𝐶 ∈ ( Met ‘ 𝑋 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
39 3 38 syl ( 𝜑𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
40 39 adantr ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
41 rpxr ( 𝑆 ∈ ℝ+𝑆 ∈ ℝ* )
42 41 ad2antll ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) → 𝑆 ∈ ℝ* )
43 blval ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥𝑋𝑆 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑆 ) = { 𝑦𝑋 ∣ ( 𝑥 𝐶 𝑦 ) < 𝑆 } )
44 40 31 42 43 syl3anc ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ 𝐶 ) 𝑆 ) = { 𝑦𝑋 ∣ ( 𝑥 𝐶 𝑦 ) < 𝑆 } )
45 27 37 44 3sstr4d ( ( 𝜑 ∧ ( 𝑥𝑋𝑆 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑆 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑆 ) )