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 = ( 𝑢 ∈ ∪ ran UnifOn ↦ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑢 ) ∣ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccfilu ⊢ CauFilu
1 vu ⊢ 𝑢
2 cust ⊢ UnifOn
3 2 crn ⊢ ran UnifOn
4 3 cuni ⊢ ∪ ran UnifOn
5 vf ⊢ 𝑓
6 cfbas ⊢ fBas
7 1 cv ⊢ 𝑢
8 7 cuni ⊢ ∪ 𝑢
9 8 cdm ⊢ dom ∪ 𝑢
10 9 6 cfv ⊢ ( fBas ‘ dom ∪ 𝑢 )
11 vv ⊢ 𝑣
12 va ⊢ 𝑎
13 5 cv ⊢ 𝑓
14 12 cv ⊢ 𝑎
15 14 14 cxp ⊢ ( 𝑎 × 𝑎 )
16 11 cv ⊢ 𝑣
17 15 16 wss ⊢ ( 𝑎 × 𝑎 ) ⊆ 𝑣
18 17 12 13 wrex ⊢ ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣
19 18 11 7 wral ⊢ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣
20 19 5 10 crab ⊢ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑢 ) ∣ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 }
21 1 4 20 cmpt ⊢ ( 𝑢 ∈ ∪ ran UnifOn ↦ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑢 ) ∣ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } )
22 0 21 wceq ⊢ CauFilu = ( 𝑢 ∈ ∪ ran UnifOn ↦ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑢 ) ∣ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } )