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

Definition df-cfilu 22312
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 22311 . 2 class CauFilu
2 vu . . 3 setvar 𝑢
3 cust 22224 . . . . 5 class UnifOn
43crn 5267 . . . 4 class ran UnifOn
54cuni 4588 . . 3 class ran UnifOn
6 va . . . . . . . . 9 setvar 𝑎
76cv 1631 . . . . . . . 8 class 𝑎
87, 7cxp 5264 . . . . . . 7 class (𝑎 × 𝑎)
9 vv . . . . . . . 8 setvar 𝑣
109cv 1631 . . . . . . 7 class 𝑣
118, 10wss 3715 . . . . . 6 wff (𝑎 × 𝑎) ⊆ 𝑣
12 vf . . . . . . 7 setvar 𝑓
1312cv 1631 . . . . . 6 class 𝑓
1411, 6, 13wrex 3051 . . . . 5 wff 𝑎𝑓 (𝑎 × 𝑎) ⊆ 𝑣
152cv 1631 . . . . 5 class 𝑢
1614, 9, 15wral 3050 . . . 4 wff 𝑣𝑢𝑎𝑓 (𝑎 × 𝑎) ⊆ 𝑣
1715cuni 4588 . . . . . 6 class 𝑢
1817cdm 5266 . . . . 5 class dom 𝑢
19 cfbas 19956 . . . . 5 class fBas
2018, 19cfv 6049 . . . 4 class (fBas‘dom 𝑢)
2116, 12, 20crab 3054 . . 3 class {𝑓 ∈ (fBas‘dom 𝑢) ∣ ∀𝑣𝑢𝑎𝑓 (𝑎 × 𝑎) ⊆ 𝑣}
222, 5, 21cmpt 4881 . 2 class (𝑢 ran UnifOn ↦ {𝑓 ∈ (fBas‘dom 𝑢) ∣ ∀𝑣𝑢𝑎𝑓 (𝑎 × 𝑎) ⊆ 𝑣})
231, 22wceq 1632 1 wff CauFilu = (𝑢 ran UnifOn ↦ {𝑓 ∈ (fBas‘dom 𝑢) ∣ ∀𝑣𝑢𝑎𝑓 (𝑎 × 𝑎) ⊆ 𝑣})
Colors of variables: wff setvar class
This definition is referenced by:  iscfilu  22313
  Copyright terms: Public domain W3C validator