Metamath Proof Explorer

Theorem ustuqtop

Description: For a given uniform structure U on a set X , there is a unique topology j such that the set ran ( v e. U |-> ( v " { p } ) ) is the filter of the neighborhoods of p for that topology. Proposition 1 of BourbakiTop1 p. II.3. (Contributed by Thierry Arnoux, 11-Jan-2018)

Ref Expression
Hypothesis utopustuq.1 ⊢N=p∈X⟼ran⁡v∈U⟼vp
Assertion ustuqtop ⊢U∈UnifOn⁡X→∃!j∈TopOn⁡X∀p∈XN⁡p=nei⁡j⁡p

Proof

Step Hyp Ref Expression
1 utopustuq.1 ⊢N=p∈X⟼ran⁡v∈U⟼vp
2 fveq2 ⊢p=r→N⁡p=N⁡r
3 2 eleq2d ⊢p=r→c∈N⁡p↔c∈N⁡r
4 3 cbvralvw ⊢∀p∈cc∈N⁡p↔∀r∈cc∈N⁡r
5 eleq1w ⊢c=a→c∈N⁡p↔a∈N⁡p
6 5 raleqbi1dv ⊢c=a→∀p∈cc∈N⁡p↔∀p∈aa∈N⁡p
7 4 6 bitr3id ⊢c=a→∀r∈cc∈N⁡r↔∀p∈aa∈N⁡p
8 7 cbvrabv ⊢c∈𝒫X|∀r∈cc∈N⁡r=a∈𝒫X|∀p∈aa∈N⁡p
9 1 ustuqtop0 ⊢U∈UnifOn⁡X→N:X⟶𝒫𝒫X
10 1 ustuqtop1 ⊢U∈UnifOn⁡X∧p∈X∧a⊆b∧b⊆X∧a∈N⁡p→b∈N⁡p
11 1 ustuqtop2 ⊢U∈UnifOn⁡X∧p∈X→fi⁡N⁡p⊆N⁡p
12 1 ustuqtop3 ⊢U∈UnifOn⁡X∧p∈X∧a∈N⁡p→p∈a
13 1 ustuqtop4 ⊢U∈UnifOn⁡X∧p∈X∧a∈N⁡p→∃b∈N⁡p∀x∈ba∈N⁡x
14 1 ustuqtop5 ⊢U∈UnifOn⁡X∧p∈X→X∈N⁡p
15 8 9 10 11 12 13 14 neiptopreu ⊢U∈UnifOn⁡X→∃!j∈TopOn⁡XN=p∈X⟼nei⁡j⁡p
16 9 feqmptd ⊢U∈UnifOn⁡X→N=p∈X⟼N⁡p
17 16 eqeq1d ⊢U∈UnifOn⁡X→N=p∈X⟼nei⁡j⁡p↔p∈X⟼N⁡p=p∈X⟼nei⁡j⁡p
18 fvex ⊢N⁡p∈V
19 18 rgenw ⊢∀p∈XN⁡p∈V
20 mpteqb ⊢∀p∈XN⁡p∈V→p∈X⟼N⁡p=p∈X⟼nei⁡j⁡p↔∀p∈XN⁡p=nei⁡j⁡p
21 19 20 ax-mp ⊢p∈X⟼N⁡p=p∈X⟼nei⁡j⁡p↔∀p∈XN⁡p=nei⁡j⁡p
22 17 21 bitrdi ⊢U∈UnifOn⁡X→N=p∈X⟼nei⁡j⁡p↔∀p∈XN⁡p=nei⁡j⁡p
23 22 reubidv ⊢U∈UnifOn⁡X→∃!j∈TopOn⁡XN=p∈X⟼nei⁡j⁡p↔∃!j∈TopOn⁡X∀p∈XN⁡p=nei⁡j⁡p
24 15 23 mpbid ⊢U∈UnifOn⁡X→∃!j∈TopOn⁡X∀p∈XN⁡p=nei⁡j⁡p