Theorem metdscn2

Description: The function F which gives the distance from a point to a nonempty set in a metric space is a continuous function into the topology of the complex numbers. (Contributed by Mario Carneiro, 5-Sep-2015)

	Ref	Expression
Hypotheses	metdscn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
	metdscn.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	metdscn2.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion	metdscn2	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
2		metdscn.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3		metdscn2.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
4		eqid	⊢ ( dist ‘ ℝ*𝑠 ) = ( dist ‘ ℝ*𝑠 )
5	4	xrsdsre	⊢ ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
6	4	xrsxmet	⊢ ( dist ‘ ℝ*𝑠 ) ∈ ( ∞Met ‘ ℝ* )
7		ressxr	⊢ ℝ ⊆ ℝ*
8		eqid	⊢ ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) ) = ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) )
9		eqid	⊢ ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) = ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) )
10		eqid	⊢ ( MetOpen ‘ ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) ) )
11	8 9 10	metrest	⊢ ( ( ( dist ‘ ℝ*𝑠 ) ∈ ( ∞Met ‘ ℝ* ) ∧ ℝ ⊆ ℝ* ) → ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) = ( MetOpen ‘ ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) ) ) )
12	6 7 11	mp2an	⊢ ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) = ( MetOpen ‘ ( ( dist ‘ ℝ*𝑠 ) ↾ ( ℝ × ℝ ) ) )
13	5 12	tgioo	⊢ ( topGen ‘ ran (,) ) = ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ )
14	3	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( 𝐾 ↾t ℝ )
15	13 14	eqtr3i	⊢ ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) = ( 𝐾 ↾t ℝ )
16	15	oveq2i	⊢ ( 𝐽 Cn ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) ) = ( 𝐽 Cn ( 𝐾 ↾t ℝ ) )
17	3	cnfldtop	⊢ 𝐾 ∈ Top
18		cnrest2r	⊢ ( 𝐾 ∈ Top → ( 𝐽 Cn ( 𝐾 ↾t ℝ ) ) ⊆ ( 𝐽 Cn 𝐾 ) )
19	17 18	ax-mp	⊢ ( 𝐽 Cn ( 𝐾 ↾t ℝ ) ) ⊆ ( 𝐽 Cn 𝐾 )
20	16 19	eqsstri	⊢ ( 𝐽 Cn ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) ) ⊆ ( 𝐽 Cn 𝐾 )
21		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
22	1 2 4 9	metdscn	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) )
23	21 22	sylan	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) )
24	23	3adant3	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → 𝐹 ∈ ( 𝐽 Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) )
25	1	metdsre	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → 𝐹 : 𝑋 ⟶ ℝ )
26		frn	⊢ ( 𝐹 : 𝑋 ⟶ ℝ → ran 𝐹 ⊆ ℝ )
27	9	mopntopon	⊢ ( ( dist ‘ ℝ*𝑠 ) ∈ ( ∞Met ‘ ℝ* ) → ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ∈ ( TopOn ‘ ℝ* ) )
28	6 27	ax-mp	⊢ ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ∈ ( TopOn ‘ ℝ* )
29		cnrest2	⊢ ( ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ∈ ( TopOn ‘ ℝ* ) ∧ ran 𝐹 ⊆ ℝ ∧ ℝ ⊆ ℝ* ) → ( 𝐹 ∈ ( 𝐽 Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) ↔ 𝐹 ∈ ( 𝐽 Cn ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) ) ) )
30	28 7 29	mp3an13	⊢ ( ran 𝐹 ⊆ ℝ → ( 𝐹 ∈ ( 𝐽 Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) ↔ 𝐹 ∈ ( 𝐽 Cn ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) ) ) )
31	25 26 30	3syl	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → ( 𝐹 ∈ ( 𝐽 Cn ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ) ↔ 𝐹 ∈ ( 𝐽 Cn ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) ) ) )
32	24 31	mpbid	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → 𝐹 ∈ ( 𝐽 Cn ( ( MetOpen ‘ ( dist ‘ ℝ*𝑠 ) ) ↾t ℝ ) ) )
33	20 32	sseldi	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅ ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )