metdscn

Description: The function F which gives the distance from a point to a set is a continuous function into the metric topology of the extended reals. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 4-Sep-2015)

	Ref	Expression
Hypotheses	metdscn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ^* , < ) )
	metdscn.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	metdscn.c	⊢ 𝐶 = ( dist ‘ ℝ^*_𝑠 )
	metdscn.k	⊢ 𝐾 = ( MetOpen ‘ 𝐶 )
Assertion	metdscn	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ^* , < ) )
2		metdscn.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3		metdscn.c	⊢ 𝐶 = ( dist ‘ ℝ^*_𝑠 )
4		metdscn.k	⊢ 𝐾 = ( MetOpen ‘ 𝐶 )
5	1	metdsf	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
6		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ^*
7		fss	⊢ ( ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ∧ ( 0 [,] +∞ ) ⊆ ℝ^* ) → 𝐹 : 𝑋 ⟶ ℝ^* )
8	5 6 7	sylancl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ℝ^* )
9		simprr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) → 𝑟 ∈ ℝ⁺ )
10	8	ad2antrr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝐹 : 𝑋 ⟶ ℝ^* )
11		simplrl	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝑧 ∈ 𝑋 )
12	10 11	ffvelcdmd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ^* )
13		simprl	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝑤 ∈ 𝑋 )
14	10 13	ffvelcdmd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ℝ^* )
15	3	xrsdsval	⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ^* ∧ ( 𝐹 ‘ 𝑤 ) ∈ ℝ^* ) → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) = if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑤 ) ) ) )
16	12 14 15	syl2anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) = if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑤 ) ) ) )
17		simplll	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
18		simpllr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝑆 ⊆ 𝑋 )
19		simplrr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝑟 ∈ ℝ⁺ )
20		xmetsym	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑤 𝐷 𝑧 ) = ( 𝑧 𝐷 𝑤 ) )
21	17 13 11 20	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝑤 𝐷 𝑧 ) = ( 𝑧 𝐷 𝑤 ) )
22		simprr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝑧 𝐷 𝑤 ) < 𝑟 )
23	21 22	eqbrtrd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝑤 𝐷 𝑧 ) < 𝑟 )
24	1 2 3 4 17 18 13 11 19 23	metdscnlem	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹 ‘ 𝑤 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑧 ) ) < 𝑟 )
25	1 2 3 4 17 18 11 13 19 22	metdscnlem	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹 ‘ 𝑧 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 )
26		breq1	⊢ ( ( ( 𝐹 ‘ 𝑤 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑧 ) ) = if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑤 ) ) ) → ( ( ( 𝐹 ‘ 𝑤 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑧 ) ) < 𝑟 ↔ if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑤 ) ) ) < 𝑟 ) )
27		breq1	⊢ ( ( ( 𝐹 ‘ 𝑧 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑤 ) ) = if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑤 ) ) ) → ( ( ( 𝐹 ‘ 𝑧 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ↔ if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑤 ) ) ) < 𝑟 ) )
28	26 27	ifboth	⊢ ( ( ( ( 𝐹 ‘ 𝑤 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑧 ) ) < 𝑟 ∧ ( ( 𝐹 ‘ 𝑧 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) → if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑤 ) ) ) < 𝑟 )
29	24 25 28	syl2anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +_𝑒 -_𝑒 ( 𝐹 ‘ 𝑤 ) ) ) < 𝑟 )
30	16 29	eqbrtrd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 )
31	30	expr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑧 𝐷 𝑤 ) < 𝑟 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) )
32	31	ralrimiva	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) → ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑟 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) )
33		breq2	⊢ ( 𝑠 = 𝑟 → ( ( 𝑧 𝐷 𝑤 ) < 𝑠 ↔ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) )
34	33	rspceaimv	⊢ ( ( 𝑟 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑟 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) ) → ∃ 𝑠 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) )
35	9 32 34	syl2anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ⁺ ) ) → ∃ 𝑠 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) )
36	35	ralrimivva	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑠 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) )
37		simpl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
38	3	xrsxmet	⊢ 𝐶 ∈ ( ∞Met ‘ ℝ^* )
39	2 4	metcn	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐶 ∈ ( ∞Met ‘ ℝ^* ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ ℝ^* ∧ ∀ 𝑧 ∈ 𝑋 ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑠 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) ) ) )
40	37 38 39	sylancl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ ℝ^* ∧ ∀ 𝑧 ∈ 𝑋 ∀ 𝑟 ∈ ℝ⁺ ∃ 𝑠 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) ) ) )
41	8 36 40	mpbir2and	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )

Metamath Proof Explorer

Theorem metdscn

Proof