cmetcusp

Description: The uniform space generated by a complete metric is a complete uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017)

		Ref	Expression
	Assertion	cmetcusp	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ∈ CUnifSp )

Proof

Step	Hyp	Ref	Expression
1		cmetmet	⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
2		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3		xmetpsmet	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
4	1 2 3	3syl	⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
5	4	anim2i	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) )
6		metuust	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) )
7		eqid	⊢ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) = ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) )
8	7	tususp	⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ∈ UnifSp )
9	5 6 8	3syl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ∈ UnifSp )
10		simpll	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )
11	10	simprd	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
12	1 2	syl	⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
13	12	ad3antlr	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
14	7	tusbas	⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) )
15	14	fveq2d	⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → ( Fil ‘ 𝑋 ) = ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) )
16	15	eleq2d	⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑐 ∈ ( Fil ‘ 𝑋 ) ↔ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) )
17	5 6 16	3syl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( 𝑐 ∈ ( Fil ‘ 𝑋 ) ↔ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) )
18	17	biimpar	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝑐 ∈ ( Fil ‘ 𝑋 ) )
19	18	adantr	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝑐 ∈ ( Fil ‘ 𝑋 ) )
20	7	tususs	⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → ( metUnif ‘ 𝐷 ) = ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) )
21	20	fveq2d	⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) = ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) )
22	5 6 21	3syl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) = ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) )
23	22	eleq2d	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( 𝑐 ∈ ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) ↔ 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) )
24	23	biimpar	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝑐 ∈ ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) )
25	24	adantlr	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝑐 ∈ ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) )
26		cfilucfil2	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ( 𝑐 ∈ ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) ↔ ( 𝑐 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝑐 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )
27	5 26	syl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( 𝑐 ∈ ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) ↔ ( 𝑐 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝑐 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )
28	27	simplbda	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( CauFil_u ‘ ( metUnif ‘ 𝐷 ) ) ) → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝑐 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) )
29	10 25 28	syl2anc	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝑐 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) )
30		iscfil	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑐 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝑐 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝑐 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )
31	30	biimpar	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑐 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ⁺ ∃ 𝑦 ∈ 𝑐 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) → 𝑐 ∈ ( CauFil ‘ 𝐷 ) )
32	13 19 29 31	syl12anc	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → 𝑐 ∈ ( CauFil ‘ 𝐷 ) )
33		eqid	⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
34	33	cmetcvg	⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝑐 ∈ ( CauFil ‘ 𝐷 ) ) → ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ≠ ∅ )
35	11 32 34	syl2anc	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ≠ ∅ )
36		eqid	⊢ ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( unifTop ‘ ( metUnif ‘ 𝐷 ) )
37	7 36	tustopn	⊢ ( ( metUnif ‘ 𝐷 ) ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) )
38	5 6 37	3syl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) )
39	12	anim2i	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) )
40		xmetutop	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) )
41	39 40	syl	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( unifTop ‘ ( metUnif ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) )
42	38 41	eqtr3d	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) = ( MetOpen ‘ 𝐷 ) )
43	42	oveq1d	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) = ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) )
44	43	neeq1d	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) ≠ ∅ ↔ ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ≠ ∅ ) )
45	44	biimpar	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ≠ ∅ ) → ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) ≠ ∅ )
46	10 35 45	syl2anc	⊢ ( ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) ∧ 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) ≠ ∅ )
47	46	ex	⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) ∧ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ) → ( 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) → ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) ≠ ∅ ) )
48	47	ralrimiva	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ( 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) → ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) ≠ ∅ ) )
49		iscusp	⊢ ( ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ∈ CUnifSp ↔ ( ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ∈ UnifSp ∧ ∀ 𝑐 ∈ ( Fil ‘ ( Base ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) ( 𝑐 ∈ ( CauFil_u ‘ ( UnifSt ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) ) → ( ( TopOpen ‘ ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ) fLim 𝑐 ) ≠ ∅ ) ) )
50	9 48 49	sylanbrc	⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) → ( toUnifSp ‘ ( metUnif ‘ 𝐷 ) ) ∈ CUnifSp )

Metamath Proof Explorer

Theorem cmetcusp

Proof