Theorem cmetcusp1 24526

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.)

Hypotheses

Ref	Expression
cmetcusp1.x	⊢ 𝑋 = (Base‘𝐹)
cmetcusp1.d	⊢ 𝐷 = ((dist‘𝐹) ↾ (𝑋 × 𝑋))
cmetcusp1.u	⊢ 𝑈 = (UnifSt‘𝐹)

Assertion

Ref	Expression
cmetcusp1	⊢ ((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) → 𝐹 ∈ CUnifSp)

Proof of Theorem cmetcusp1

Dummy variable 𝑐 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cmsms 24521	. . . 4 ⊢ (𝐹 ∈ CMetSp → 𝐹 ∈ MetSp)
2		msxms 23616	. . . 4 ⊢ (𝐹 ∈ MetSp → 𝐹 ∈ ∞MetSp)
3	1, 2	syl 17	. . 3 ⊢ (𝐹 ∈ CMetSp → 𝐹 ∈ ∞MetSp)
4		cmetcusp1.x	. . . 4 ⊢ 𝑋 = (Base‘𝐹)
5		cmetcusp1.d	. . . 4 ⊢ 𝐷 = ((dist‘𝐹) ↾ (𝑋 × 𝑋))
6		cmetcusp1.u	. . . 4 ⊢ 𝑈 = (UnifSt‘𝐹)
7	4, 5, 6	xmsusp 23734	. . 3 ⊢ ((𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = (metUnif‘𝐷)) → 𝐹 ∈ UnifSp)
8	3, 7	syl3an2 1163	. 2 ⊢ ((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) → 𝐹 ∈ UnifSp)
9		simpl3 1192	. . . . . . 7 ⊢ (((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) ∧ 𝑐 ∈ (Fil‘𝑋)) → 𝑈 = (metUnif‘𝐷))
10	9	fveq2d 6787	. . . . . 6 ⊢ (((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) ∧ 𝑐 ∈ (Fil‘𝑋)) → (CauFilu‘𝑈) = (CauFilu‘(metUnif‘𝐷)))
11	10	eleq2d 2825	. . . . 5 ⊢ (((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) ∧ 𝑐 ∈ (Fil‘𝑋)) → (𝑐 ∈ (CauFilu‘𝑈) ↔ 𝑐 ∈ (CauFilu‘(metUnif‘𝐷))))
12		simpl1 1190	. . . . . 6 ⊢ (((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) ∧ 𝑐 ∈ (Fil‘𝑋)) → 𝑋 ≠ ∅)
13	4, 5	cmscmet 24519	. . . . . . . . 9 ⊢ (𝐹 ∈ CMetSp → 𝐷 ∈ (CMet‘𝑋))
14		cmetmet 24459	. . . . . . . . 9 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
15		metxmet 23496	. . . . . . . . 9 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
16	13, 14, 15	3syl 18	. . . . . . . 8 ⊢ (𝐹 ∈ CMetSp → 𝐷 ∈ (∞Met‘𝑋))
17	16	3ad2ant2 1133	. . . . . . 7 ⊢ ((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) → 𝐷 ∈ (∞Met‘𝑋))
18	17	adantr 481	. . . . . 6 ⊢ (((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) ∧ 𝑐 ∈ (Fil‘𝑋)) → 𝐷 ∈ (∞Met‘𝑋))
19		simpr 485	. . . . . 6 ⊢ (((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) ∧ 𝑐 ∈ (Fil‘𝑋)) → 𝑐 ∈ (Fil‘𝑋))
20		cfilucfil4 24494	. . . . . 6 ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (∞Met‘𝑋) ∧ 𝑐 ∈ (Fil‘𝑋)) → (𝑐 ∈ (CauFilu‘(metUnif‘𝐷)) ↔ 𝑐 ∈ (CauFil‘𝐷)))
21	12, 18, 19, 20	syl3anc 1370	. . . . 5 ⊢ (((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) ∧ 𝑐 ∈ (Fil‘𝑋)) → (𝑐 ∈ (CauFilu‘(metUnif‘𝐷)) ↔ 𝑐 ∈ (CauFil‘𝐷)))
22	11, 21	bitrd 278	. . . 4 ⊢ (((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) ∧ 𝑐 ∈ (Fil‘𝑋)) → (𝑐 ∈ (CauFilu‘𝑈) ↔ 𝑐 ∈ (CauFil‘𝐷)))
23		eqid 2739	. . . . . . . . . . . 12 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
24	23	iscmet 24457	. . . . . . . . . . 11 ⊢ (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑐 ∈ (CauFil‘𝐷)((MetOpen‘𝐷) fLim 𝑐) ≠ ∅))
25	24	simprbi 497	. . . . . . . . . 10 ⊢ (𝐷 ∈ (CMet‘𝑋) → ∀𝑐 ∈ (CauFil‘𝐷)((MetOpen‘𝐷) fLim 𝑐) ≠ ∅)
26	13, 25	syl 17	. . . . . . . . 9 ⊢ (𝐹 ∈ CMetSp → ∀𝑐 ∈ (CauFil‘𝐷)((MetOpen‘𝐷) fLim 𝑐) ≠ ∅)
27		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘𝐹) = (TopOpen‘𝐹)
28	27, 4, 5	xmstopn 23613	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ ∞MetSp → (TopOpen‘𝐹) = (MetOpen‘𝐷))
29	3, 28	syl 17	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ CMetSp → (TopOpen‘𝐹) = (MetOpen‘𝐷))
30	29	oveq1d 7299	. . . . . . . . . . 11 ⊢ (𝐹 ∈ CMetSp → ((TopOpen‘𝐹) fLim 𝑐) = ((MetOpen‘𝐷) fLim 𝑐))
31	30	neeq1d 3004	. . . . . . . . . 10 ⊢ (𝐹 ∈ CMetSp → (((TopOpen‘𝐹) fLim 𝑐) ≠ ∅ ↔ ((MetOpen‘𝐷) fLim 𝑐) ≠ ∅))
32	31	ralbidv 3113	. . . . . . . . 9 ⊢ (𝐹 ∈ CMetSp → (∀𝑐 ∈ (CauFil‘𝐷)((TopOpen‘𝐹) fLim 𝑐) ≠ ∅ ↔ ∀𝑐 ∈ (CauFil‘𝐷)((MetOpen‘𝐷) fLim 𝑐) ≠ ∅))
33	26, 32	mpbird 256	. . . . . . . 8 ⊢ (𝐹 ∈ CMetSp → ∀𝑐 ∈ (CauFil‘𝐷)((TopOpen‘𝐹) fLim 𝑐) ≠ ∅)
34	33	r19.21bi 3135	. . . . . . 7 ⊢ ((𝐹 ∈ CMetSp ∧ 𝑐 ∈ (CauFil‘𝐷)) → ((TopOpen‘𝐹) fLim 𝑐) ≠ ∅)
35	34	ex 413	. . . . . 6 ⊢ (𝐹 ∈ CMetSp → (𝑐 ∈ (CauFil‘𝐷) → ((TopOpen‘𝐹) fLim 𝑐) ≠ ∅))
36	35	3ad2ant2 1133	. . . . 5 ⊢ ((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) → (𝑐 ∈ (CauFil‘𝐷) → ((TopOpen‘𝐹) fLim 𝑐) ≠ ∅))
37	36	adantr 481	. . . 4 ⊢ (((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) ∧ 𝑐 ∈ (Fil‘𝑋)) → (𝑐 ∈ (CauFil‘𝐷) → ((TopOpen‘𝐹) fLim 𝑐) ≠ ∅))
38	22, 37	sylbid 239	. . 3 ⊢ (((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) ∧ 𝑐 ∈ (Fil‘𝑋)) → (𝑐 ∈ (CauFilu‘𝑈) → ((TopOpen‘𝐹) fLim 𝑐) ≠ ∅))
39	38	ralrimiva 3104	. 2 ⊢ ((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) → ∀𝑐 ∈ (Fil‘𝑋)(𝑐 ∈ (CauFilu‘𝑈) → ((TopOpen‘𝐹) fLim 𝑐) ≠ ∅))
40	4, 6, 27	iscusp2 23463	. 2 ⊢ (𝐹 ∈ CUnifSp ↔ (𝐹 ∈ UnifSp ∧ ∀𝑐 ∈ (Fil‘𝑋)(𝑐 ∈ (CauFilu‘𝑈) → ((TopOpen‘𝐹) fLim 𝑐) ≠ ∅)))
41	8, 39, 40	sylanbrc 583	1 ⊢ ((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) → 𝐹 ∈ CUnifSp)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   ≠ wne 2944  ∀wral 3065  ∅c0 4257   × cxp 5588   ↾ cres 5592  ‘cfv 6437  (class class class)co 7284  Basecbs 16921  distcds 16980  TopOpenctopn 17141  ∞Metcxmet 20591  Metcmet 20592  MetOpencmopn 20596  metUnifcmetu 20597  Filcfil 23005   fLim cflim 23094  UnifStcuss 23414  UnifSpcusp 23415  CauFil_uccfilu 23447  CUnifSpccusp 23458  ∞MetSpcxms 23479  MetSpcms 23480  CauFilccfil 24425  CMetccmet 24427  CMetSpccms 24505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957  ax-pre-sup 10958

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-1st 7840  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-er 8507  df-map 8626  df-en 8743  df-dom 8744  df-sdom 8745  df-sup 9210  df-inf 9211  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-div 11642  df-nn 11983  df-2 12045  df-n0 12243  df-z 12329  df-uz 12592  df-q 12698  df-rp 12740  df-xneg 12857  df-xadd 12858  df-xmul 12859  df-ico 13094  df-topgen 17163  df-psmet 20598  df-xmet 20599  df-met 20600  df-bl 20601  df-mopn 20602  df-fbas 20603  df-fg 20604  df-metu 20605  df-top 22052  df-topon 22069  df-topsp 22091  df-bases 22105  df-fil 23006  df-ust 23361  df-utop 23392  df-usp 23418  df-cfilu 23448  df-cusp 23459  df-xms 23482  df-ms 23483  df-cfil 24428  df-cmet 24430  df-cms 24508

This theorem is referenced by:  cnfldcusp  24530  recusp  24555