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 ‘ 𝐶 ) 𝑆 ) )