Metamath Proof Explorer

Theorem cmetcusp1

Description: If the uniform set of a complete metric space is the uniform structure generated by its metric, then it is a complete uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017)

Ref Expression
Hypotheses cmetcusp1.x ⊢ 𝑋 = ( Base ‘ 𝐹 )
cmetcusp1.d ⊢ 𝐷 = ( ( dist ‘ 𝐹 ) ↾ ( 𝑋 × 𝑋 ) )
cmetcusp1.u ⊢ 𝑈 = ( UnifSt ‘ 𝐹 )
Assertion cmetcusp1 ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → 𝐹 ∈ CUnifSp )

Proof

Step Hyp Ref Expression
1 cmetcusp1.x ⊢ 𝑋 = ( Base ‘ 𝐹 )
2 cmetcusp1.d ⊢ 𝐷 = ( ( dist ‘ 𝐹 ) ↾ ( 𝑋 × 𝑋 ) )
3 cmetcusp1.u ⊢ 𝑈 = ( UnifSt ‘ 𝐹 )
4 cmsms ⊢ ( 𝐹 ∈ CMetSp → 𝐹 ∈ MetSp )
5 msxms ⊢ ( 𝐹 ∈ MetSp → 𝐹 ∈ ∞MetSp )
6 4 5 syl ⊢ ( 𝐹 ∈ CMetSp → 𝐹 ∈ ∞MetSp )
7 1 2 3 xmsusp ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → 𝐹 ∈ UnifSp )
8 6 7 syl3an2 ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → 𝐹 ∈ UnifSp )
9 simpl3 ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) ∧ 𝑐 ∈ ( Fil ‘ 𝑋 ) ) → 𝑈 = ( metUnif ‘ 𝐷 ) )
10 9 fveq2d ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) ∧ 𝑐 ∈ ( Fil ‘ 𝑋 ) ) → ( CauFilu ‘ 𝑈 ) = ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) )
11 10 eleq2d ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) ∧ 𝑐 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑐 ∈ ( CauFilu ‘ 𝑈 ) ↔ 𝑐 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ) )
12 simpl1 ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) ∧ 𝑐 ∈ ( Fil ‘ 𝑋 ) ) → 𝑋 ≠ ∅ )
13 1 2 cmscmet ⊢ ( 𝐹 ∈ CMetSp → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
14 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
15 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
16 13 14 15 3syl ⊢ ( 𝐹 ∈ CMetSp → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
17 16 3ad2ant2 ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
18 17 adantr ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) ∧ 𝑐 ∈ ( Fil ‘ 𝑋 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
19 simpr ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) ∧ 𝑐 ∈ ( Fil ‘ 𝑋 ) ) → 𝑐 ∈ ( Fil ‘ 𝑋 ) )
20 cfilucfil4 ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑐 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑐 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ↔ 𝑐 ∈ ( CauFil ‘ 𝐷 ) ) )
21 12 18 19 20 syl3anc ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) ∧ 𝑐 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑐 ∈ ( CauFilu ‘ ( metUnif ‘ 𝐷 ) ) ↔ 𝑐 ∈ ( CauFil ‘ 𝐷 ) ) )
22 11 21 bitrd ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) ∧ 𝑐 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑐 ∈ ( CauFilu ‘ 𝑈 ) ↔ 𝑐 ∈ ( CauFil ‘ 𝐷 ) ) )
23 eqid ⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 )
24 23 iscmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ↔ ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ∀ 𝑐 ∈ ( CauFil ‘ 𝐷 ) ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ≠ ∅ ) )
25 24 simprbi ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → ∀ 𝑐 ∈ ( CauFil ‘ 𝐷 ) ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ≠ ∅ )
26 13 25 syl ⊢ ( 𝐹 ∈ CMetSp → ∀ 𝑐 ∈ ( CauFil ‘ 𝐷 ) ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ≠ ∅ )
27 eqid ⊢ ( TopOpen ‘ 𝐹 ) = ( TopOpen ‘ 𝐹 )
28 27 1 2 xmstopn ⊢ ( 𝐹 ∈ ∞MetSp → ( TopOpen ‘ 𝐹 ) = ( MetOpen ‘ 𝐷 ) )
29 6 28 syl ⊢ ( 𝐹 ∈ CMetSp → ( TopOpen ‘ 𝐹 ) = ( MetOpen ‘ 𝐷 ) )
30 29 oveq1d ⊢ ( 𝐹 ∈ CMetSp → ( ( TopOpen ‘ 𝐹 ) fLim 𝑐 ) = ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) )
31 30 neeq1d ⊢ ( 𝐹 ∈ CMetSp → ( ( ( TopOpen ‘ 𝐹 ) fLim 𝑐 ) ≠ ∅ ↔ ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ≠ ∅ ) )
32 31 ralbidv ⊢ ( 𝐹 ∈ CMetSp → ( ∀ 𝑐 ∈ ( CauFil ‘ 𝐷 ) ( ( TopOpen ‘ 𝐹 ) fLim 𝑐 ) ≠ ∅ ↔ ∀ 𝑐 ∈ ( CauFil ‘ 𝐷 ) ( ( MetOpen ‘ 𝐷 ) fLim 𝑐 ) ≠ ∅ ) )
33 26 32 mpbird ⊢ ( 𝐹 ∈ CMetSp → ∀ 𝑐 ∈ ( CauFil ‘ 𝐷 ) ( ( TopOpen ‘ 𝐹 ) fLim 𝑐 ) ≠ ∅ )
34 33 r19.21bi ⊢ ( ( 𝐹 ∈ CMetSp ∧ 𝑐 ∈ ( CauFil ‘ 𝐷 ) ) → ( ( TopOpen ‘ 𝐹 ) fLim 𝑐 ) ≠ ∅ )
35 34 ex ⊢ ( 𝐹 ∈ CMetSp → ( 𝑐 ∈ ( CauFil ‘ 𝐷 ) → ( ( TopOpen ‘ 𝐹 ) fLim 𝑐 ) ≠ ∅ ) )
36 35 3ad2ant2 ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → ( 𝑐 ∈ ( CauFil ‘ 𝐷 ) → ( ( TopOpen ‘ 𝐹 ) fLim 𝑐 ) ≠ ∅ ) )
37 36 adantr ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) ∧ 𝑐 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑐 ∈ ( CauFil ‘ 𝐷 ) → ( ( TopOpen ‘ 𝐹 ) fLim 𝑐 ) ≠ ∅ ) )
38 22 37 sylbid ⊢ ( ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) ∧ 𝑐 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑐 ∈ ( CauFilu ‘ 𝑈 ) → ( ( TopOpen ‘ 𝐹 ) fLim 𝑐 ) ≠ ∅ ) )
39 38 ralrimiva ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → ∀ 𝑐 ∈ ( Fil ‘ 𝑋 ) ( 𝑐 ∈ ( CauFilu ‘ 𝑈 ) → ( ( TopOpen ‘ 𝐹 ) fLim 𝑐 ) ≠ ∅ ) )
40 1 3 27 iscusp2 ⊢ ( 𝐹 ∈ CUnifSp ↔ ( 𝐹 ∈ UnifSp ∧ ∀ 𝑐 ∈ ( Fil ‘ 𝑋 ) ( 𝑐 ∈ ( CauFilu ‘ 𝑈 ) → ( ( TopOpen ‘ 𝐹 ) fLim 𝑐 ) ≠ ∅ ) ) )
41 8 39 40 sylanbrc ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = ( metUnif ‘ 𝐷 ) ) → 𝐹 ∈ CUnifSp )