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

Theorem cuspcvg 23806
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 2822 . . . . 5 (𝑐 = 𝐢 β†’ (𝑐 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) ↔ 𝐢 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š))))
2 cuspcvg.2 . . . . . . . . 9 𝐽 = (TopOpenβ€˜π‘Š)
32eqcomi 2742 . . . . . . . 8 (TopOpenβ€˜π‘Š) = 𝐽
43a1i 11 . . . . . . 7 (𝑐 = 𝐢 β†’ (TopOpenβ€˜π‘Š) = 𝐽)
5 id 22 . . . . . . 7 (𝑐 = 𝐢 β†’ 𝑐 = 𝐢)
64, 5oveq12d 7427 . . . . . 6 (𝑐 = 𝐢 β†’ ((TopOpenβ€˜π‘Š) fLim 𝑐) = (𝐽 fLim 𝐢))
76neeq1d 3001 . . . . 5 (𝑐 = 𝐢 β†’ (((TopOpenβ€˜π‘Š) fLim 𝑐) β‰  βˆ… ↔ (𝐽 fLim 𝐢) β‰  βˆ…))
81, 7imbi12d 345 . . . 4 (𝑐 = 𝐢 β†’ ((𝑐 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) β†’ ((TopOpenβ€˜π‘Š) fLim 𝑐) β‰  βˆ…) ↔ (𝐢 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) β†’ (𝐽 fLim 𝐢) β‰  βˆ…)))
9 iscusp 23804 . . . . . 6 (π‘Š ∈ CUnifSp ↔ (π‘Š ∈ UnifSp ∧ βˆ€π‘ ∈ (Filβ€˜(Baseβ€˜π‘Š))(𝑐 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) β†’ ((TopOpenβ€˜π‘Š) fLim 𝑐) β‰  βˆ…)))
109simprbi 498 . . . . 5 (π‘Š ∈ CUnifSp β†’ βˆ€π‘ ∈ (Filβ€˜(Baseβ€˜π‘Š))(𝑐 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) β†’ ((TopOpenβ€˜π‘Š) fLim 𝑐) β‰  βˆ…))
1110adantr 482 . . . 4 ((π‘Š ∈ CUnifSp ∧ 𝐢 ∈ (Filβ€˜π΅)) β†’ βˆ€π‘ ∈ (Filβ€˜(Baseβ€˜π‘Š))(𝑐 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) β†’ ((TopOpenβ€˜π‘Š) fLim 𝑐) β‰  βˆ…))
12 simpr 486 . . . . 5 ((π‘Š ∈ CUnifSp ∧ 𝐢 ∈ (Filβ€˜π΅)) β†’ 𝐢 ∈ (Filβ€˜π΅))
13 cuspcvg.1 . . . . . 6 𝐡 = (Baseβ€˜π‘Š)
1413fveq2i 6895 . . . . 5 (Filβ€˜π΅) = (Filβ€˜(Baseβ€˜π‘Š))
1512, 14eleqtrdi 2844 . . . 4 ((π‘Š ∈ CUnifSp ∧ 𝐢 ∈ (Filβ€˜π΅)) β†’ 𝐢 ∈ (Filβ€˜(Baseβ€˜π‘Š)))
168, 11, 15rspcdva 3614 . . 3 ((π‘Š ∈ CUnifSp ∧ 𝐢 ∈ (Filβ€˜π΅)) β†’ (𝐢 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) β†’ (𝐽 fLim 𝐢) β‰  βˆ…))
17163impia 1118 . 2 ((π‘Š ∈ CUnifSp ∧ 𝐢 ∈ (Filβ€˜π΅) ∧ 𝐢 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š))) β†’ (𝐽 fLim 𝐢) β‰  βˆ…)
18173com23 1127 1 ((π‘Š ∈ CUnifSp ∧ 𝐢 ∈ (CauFiluβ€˜(UnifStβ€˜π‘Š)) ∧ 𝐢 ∈ (Filβ€˜π΅)) β†’ (𝐽 fLim 𝐢) β‰  βˆ…)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆ…c0 4323  β€˜cfv 6544  (class class class)co 7409  Basecbs 17144  TopOpenctopn 17367  Filcfil 23349   fLim cflim 23438  UnifStcuss 23758  UnifSpcusp 23759  CauFiluccfilu 23791  CUnifSpccusp 23802
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-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-cusp 23803
This theorem is referenced by:  cnextucn  23808
  Copyright terms: Public domain W3C validator