This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cfilu

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 v , there is an element a of the filter "small enough in v " i.e. such that every pair { x , y } of points in a is related by v ". Definition 2 of BourbakiTop1 p. II.13. (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion df-cfilu ⊢ CauFilU = u ∈ ⋃ ran ⁡ UnifOn ⟼ f ∈ fBas ⁡ dom ⁡ ⋃ u | ∀ v ∈ u ∃ a ∈ f a × a ⊆ v

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccfilu class CauFilU
1 vu setvar u
2 cust class UnifOn
3 2 crn class ran ⁡ UnifOn
4 3 cuni class ⋃ ran ⁡ UnifOn
5 vf setvar f
6 cfbas class fBas
7 1 cv setvar u
8 7 cuni class ⋃ u
9 8 cdm class dom ⁡ ⋃ u
10 9 6 cfv class fBas ⁡ dom ⁡ ⋃ u
11 vv setvar v
12 va setvar a
13 5 cv setvar f
14 12 cv setvar a
15 14 14 cxp class a × a
16 11 cv setvar v
17 15 16 wss wff a × a ⊆ v
18 17 12 13 wrex wff ∃ a ∈ f a × a ⊆ v
19 18 11 7 wral wff ∀ v ∈ u ∃ a ∈ f a × a ⊆ v
20 19 5 10 crab class f ∈ fBas ⁡ dom ⁡ ⋃ u | ∀ v ∈ u ∃ a ∈ f a × a ⊆ v
21 1 4 20 cmpt class u ∈ ⋃ ran ⁡ UnifOn ⟼ f ∈ fBas ⁡ dom ⁡ ⋃ u | ∀ v ∈ u ∃ a ∈ f a × a ⊆ v
22 0 21 wceq wff CauFilU = u ∈ ⋃ ran ⁡ UnifOn ⟼ f ∈ fBas ⁡ dom ⁡ ⋃ u | ∀ v ∈ u ∃ a ∈ f a × a ⊆ v