MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cuspcvg Structured version   Visualization version   GIF version

Theorem cuspcvg 24026
Description: In a complete uniform space, any Cauchy filter 𝐢 has a limit. (Contributed by Thierry Arnoux, 3-Dec-2017.)
Hypotheses
Ref Expression
cuspcvg.1 𝐡 = (Baseβ€˜π‘Š)
cuspcvg.2 𝐽 = (TopOpenβ€˜π‘Š)
Assertion
Ref Expression
cuspcvg ((π‘Š ∈ CUnifSp ∧ 𝐢 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) ∧ 𝐢 ∈ (Filβ€˜π΅)) β†’ (𝐽 fLim 𝐢) β‰  βˆ…)

Proof of Theorem cuspcvg
Dummy variable 𝑐 is distinct from all other variables.
StepHypRef Expression
1 eleq1 2819 . . . . 5 (𝑐 = 𝐢 β†’ (𝑐 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) ↔ 𝐢 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š))))
2 cuspcvg.2 . . . . . . . . 9 𝐽 = (TopOpenβ€˜π‘Š)
32eqcomi 2739 . . . . . . . 8 (TopOpenβ€˜π‘Š) = 𝐽
43a1i 11 . . . . . . 7 (𝑐 = 𝐢 β†’ (TopOpenβ€˜π‘Š) = 𝐽)
5 id 22 . . . . . . 7 (𝑐 = 𝐢 β†’ 𝑐 = 𝐢)
64, 5oveq12d 7429 . . . . . 6 (𝑐 = 𝐢 β†’ ((TopOpenβ€˜π‘Š) fLim 𝑐) = (𝐽 fLim 𝐢))
76neeq1d 2998 . . . . 5 (𝑐 = 𝐢 β†’ (((TopOpenβ€˜π‘Š) fLim 𝑐) β‰  βˆ… ↔ (𝐽 fLim 𝐢) β‰  βˆ…))
81, 7imbi12d 343 . . . 4 (𝑐 = 𝐢 β†’ ((𝑐 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) β†’ ((TopOpenβ€˜π‘Š) fLim 𝑐) β‰  βˆ…) ↔ (𝐢 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) β†’ (𝐽 fLim 𝐢) β‰  βˆ…)))
9 iscusp 24024 . . . . . 6 (π‘Š ∈ CUnifSp ↔ (π‘Š ∈ UnifSp ∧ βˆ€π‘ ∈ (Filβ€˜(Baseβ€˜π‘Š))(𝑐 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) β†’ ((TopOpenβ€˜π‘Š) fLim 𝑐) β‰  βˆ…)))
109simprbi 495 . . . . 5 (π‘Š ∈ CUnifSp β†’ βˆ€π‘ ∈ (Filβ€˜(Baseβ€˜π‘Š))(𝑐 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) β†’ ((TopOpenβ€˜π‘Š) fLim 𝑐) β‰  βˆ…))
1110adantr 479 . . . 4 ((π‘Š ∈ CUnifSp ∧ 𝐢 ∈ (Filβ€˜π΅)) β†’ βˆ€π‘ ∈ (Filβ€˜(Baseβ€˜π‘Š))(𝑐 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) β†’ ((TopOpenβ€˜π‘Š) fLim 𝑐) β‰  βˆ…))
12 simpr 483 . . . . 5 ((π‘Š ∈ CUnifSp ∧ 𝐢 ∈ (Filβ€˜π΅)) β†’ 𝐢 ∈ (Filβ€˜π΅))
13 cuspcvg.1 . . . . . 6 𝐡 = (Baseβ€˜π‘Š)
1413fveq2i 6893 . . . . 5 (Filβ€˜π΅) = (Filβ€˜(Baseβ€˜π‘Š))
1512, 14eleqtrdi 2841 . . . 4 ((π‘Š ∈ CUnifSp ∧ 𝐢 ∈ (Filβ€˜π΅)) β†’ 𝐢 ∈ (Filβ€˜(Baseβ€˜π‘Š)))
168, 11, 15rspcdva 3612 . . 3 ((π‘Š ∈ CUnifSp ∧ 𝐢 ∈ (Filβ€˜π΅)) β†’ (𝐢 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) β†’ (𝐽 fLim 𝐢) β‰  βˆ…))
17163impia 1115 . 2 ((π‘Š ∈ CUnifSp ∧ 𝐢 ∈ (Filβ€˜π΅) ∧ 𝐢 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š))) β†’ (𝐽 fLim 𝐢) β‰  βˆ…)
18173com23 1124 1 ((π‘Š ∈ CUnifSp ∧ 𝐢 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) ∧ 𝐢 ∈ (Filβ€˜π΅)) β†’ (𝐽 fLim 𝐢) β‰  βˆ…)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆ…c0 4321  β€˜cfv 6542  (class class class)co 7411  Basecbs 17148  TopOpenctopn 17371  Filcfil 23569   fLim cflim 23658  UnifStcuss 23978  UnifSpcusp 23979  CauFiluccfilu 24011  CUnifSpccusp 24022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414  df-cusp 24023
This theorem is referenced by:  cnextucn  24028
  Copyright terms: Public domain W3C validator