Theorem metss2

Description: If the metric D is "strongly finer" than C (meaning that there is a positive real constant R such that C ( x , y ) <_ R x. D ( x , y ) ), then D generates a finer topology. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they generate the same topology.) (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	metss2	⊢ ( 𝜑 → 𝐽 ⊆ 𝐾 )

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		simpr	⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
8		rpdivcl	⊢ ( ( 𝑟 ∈ ℝ+ ∧ 𝑅 ∈ ℝ+ ) → ( 𝑟 / 𝑅 ) ∈ ℝ+ )
9	7 5 8	syl2anr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑟 / 𝑅 ) ∈ ℝ+ )
10	1 2 3 4 5 6	metss2lem	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) )
11		oveq2	⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) = ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) )
12	11	sseq1d	⊢ ( 𝑠 = ( 𝑟 / 𝑅 ) → ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ↔ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
13	12	rspcev	⊢ ( ( ( 𝑟 / 𝑅 ) ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 𝑅 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) )
14	9 10 13	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) )
15	14	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) )
16		metxmet	⊢ ( 𝐶 ∈ ( Met ‘ 𝑋 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
17	3 16	syl	⊢ ( 𝜑 → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
18		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
19	4 18	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
20	1 2	metss	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( 𝐽 ⊆ 𝐾 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
21	17 19 20	syl2anc	⊢ ( 𝜑 → ( 𝐽 ⊆ 𝐾 ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑠 ) ⊆ ( 𝑥 ( ball ‘ 𝐶 ) 𝑟 ) ) )
22	15 21	mpbird	⊢ ( 𝜑 → 𝐽 ⊆ 𝐾 )