Theorem xmetdcn2

Description: The metric function of an extended metric space is always continuous in the topology generated by it. In this variation of xmetdcn we use the metric topology instead of the order topology on RR* , which makes the theorem a bit stronger. Since +oo is an isolated point in the metric topology, this is saying that for any points A , B which are an infinite distance apart, there is a product neighborhood around <. A , B >. such that d ( a , b ) = +oo for any a near A and b near B , i.e., the distance function is locally constant +oo . (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 4-Sep-2015)

	Ref	Expression
Hypotheses	xmetdcn2.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	xmetdcn2.2	⊢ 𝐶 = ( dist ‘ ℝ*𝑠 )
	xmetdcn2.3	⊢ 𝐾 = ( MetOpen ‘ 𝐶 )
Assertion	xmetdcn2	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		xmetdcn2.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		xmetdcn2.2	⊢ 𝐶 = ( dist ‘ ℝ*𝑠 )
3		xmetdcn2.3	⊢ 𝐾 = ( MetOpen ‘ 𝐶 )
4		xmetf	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
5		rphalfcl	⊢ ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) ∈ ℝ+ )
6		simp-4l	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
7		simplrl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑥 ∈ 𝑋 )
8	7	ad2antrr	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) ) → 𝑥 ∈ 𝑋 )
9		simplrr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑦 ∈ 𝑋 )
10	9	ad2antrr	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) ) → 𝑦 ∈ 𝑋 )
11		simpllr	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) ) → 𝑟 ∈ ℝ+ )
12		simplrl	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) ) → 𝑧 ∈ 𝑋 )
13		simplrr	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) ) → 𝑤 ∈ 𝑋 )
14		simprl	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) ) → ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) )
15		simprr	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) ) → ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) )
16	1 2 3 6 8 10 11 12 13 14 15	metdcnlem	⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 )
17	16	ex	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 ) )
18	17	ralrimivva	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 ) )
19		breq2	⊢ ( 𝑠 = ( 𝑟 / 2 ) → ( ( 𝑥 𝐷 𝑧 ) < 𝑠 ↔ ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ) )
20		breq2	⊢ ( 𝑠 = ( 𝑟 / 2 ) → ( ( 𝑦 𝐷 𝑤 ) < 𝑠 ↔ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) )
21	19 20	anbi12d	⊢ ( 𝑠 = ( 𝑟 / 2 ) → ( ( ( 𝑥 𝐷 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐷 𝑤 ) < 𝑠 ) ↔ ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) ) )
22	21	imbi1d	⊢ ( 𝑠 = ( 𝑟 / 2 ) → ( ( ( ( 𝑥 𝐷 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐷 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 ) ↔ ( ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 ) ) )
23	22	2ralbidv	⊢ ( 𝑠 = ( 𝑟 / 2 ) → ( ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐷 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 ) ) )
24	23	rspcev	⊢ ( ( ( 𝑟 / 2 ) ∈ ℝ+ ∧ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑧 ) < ( 𝑟 / 2 ) ∧ ( 𝑦 𝐷 𝑤 ) < ( 𝑟 / 2 ) ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 ) ) → ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐷 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 ) )
25	5 18 24	syl2an2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐷 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 ) )
26	25	ralrimiva	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐷 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 ) )
27	26	ralrimivva	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐷 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 ) )
28		id	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
29	2	xrsxmet	⊢ 𝐶 ∈ ( ∞Met ‘ ℝ* )
30	29	a1i	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐶 ∈ ( ∞Met ‘ ℝ* ) )
31	1 1 3	txmetcn	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐶 ∈ ( ∞Met ‘ ℝ* ) ) → ( 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐷 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 ) ) ) )
32	28 30 31	mpd3an23	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) ↔ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( ( 𝑥 𝐷 𝑧 ) < 𝑠 ∧ ( 𝑦 𝐷 𝑤 ) < 𝑠 ) → ( ( 𝑥 𝐷 𝑦 ) 𝐶 ( 𝑧 𝐷 𝑤 ) ) < 𝑟 ) ) ) )
33	4 27 32	mpbir2and	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )