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 )