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

Definition df-cfilu 22888
 Description: Define the set of Cauchy filter bases on a uniform space. A Cauchy filter base is a filter base on the set such that for every entourage 𝑣, there is an element 𝑎 of the filter "small enough in 𝑣 " i.e. such that every pair {𝑥, 𝑦} of points in 𝑎 is related by 𝑣". Definition 2 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 16-Nov-2017.)
Assertion
Ref Expression
df-cfilu CauFilu = (𝑢 ran UnifOn ↦ {𝑓 ∈ (fBas‘dom 𝑢) ∣ ∀𝑣𝑢𝑎𝑓 (𝑎 × 𝑎) ⊆ 𝑣})
Distinct variable group:   𝑢,𝑓,𝑣,𝑎

Detailed syntax breakdown of Definition df-cfilu
StepHypRef Expression
1 ccfilu 22887 . 2 class CauFilu
2 vu . . 3 setvar 𝑢
3 cust 22800 . . . . 5 class UnifOn
43crn 5549 . . . 4 class ran UnifOn
54cuni 4830 . . 3 class ran UnifOn
6 va . . . . . . . . 9 setvar 𝑎
76cv 1530 . . . . . . . 8 class 𝑎
87, 7cxp 5546 . . . . . . 7 class (𝑎 × 𝑎)
9 vv . . . . . . . 8 setvar 𝑣
109cv 1530 . . . . . . 7 class 𝑣
118, 10wss 3934 . . . . . 6 wff (𝑎 × 𝑎) ⊆ 𝑣
12 vf . . . . . . 7 setvar 𝑓
1312cv 1530 . . . . . 6 class 𝑓
1411, 6, 13wrex 3137 . . . . 5 wff 𝑎𝑓 (𝑎 × 𝑎) ⊆ 𝑣
152cv 1530 . . . . 5 class 𝑢
1614, 9, 15wral 3136 . . . 4 wff 𝑣𝑢𝑎𝑓 (𝑎 × 𝑎) ⊆ 𝑣
1715cuni 4830 . . . . . 6 class 𝑢
1817cdm 5548 . . . . 5 class dom 𝑢
19 cfbas 20525 . . . . 5 class fBas
2018, 19cfv 6348 . . . 4 class (fBas‘dom 𝑢)
2116, 12, 20crab 3140 . . 3 class {𝑓 ∈ (fBas‘dom 𝑢) ∣ ∀𝑣𝑢𝑎𝑓 (𝑎 × 𝑎) ⊆ 𝑣}
222, 5, 21cmpt 5137 . 2 class (𝑢 ran UnifOn ↦ {𝑓 ∈ (fBas‘dom 𝑢) ∣ ∀𝑣𝑢𝑎𝑓 (𝑎 × 𝑎) ⊆ 𝑣})
231, 22wceq 1531 1 wff CauFilu = (𝑢 ran UnifOn ↦ {𝑓 ∈ (fBas‘dom 𝑢) ∣ ∀𝑣𝑢𝑎𝑓 (𝑎 × 𝑎) ⊆ 𝑣})
 Colors of variables: wff setvar class This definition is referenced by:  iscfilu  22889
 Copyright terms: Public domain W3C validator