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 v p
Assertion ustuqtop U UnifOn X ∃! j TopOn X p X N p = nei j p

Proof

Step Hyp Ref Expression
1 utopustuq.1 N = p X ran v U v p
2 fveq2 p = r N p = N r
3 2 eleq2d p = r c N p c N r
4 3 cbvralvw p c c N p r c c N r
5 eleq1w c = a c N p a N p
6 5 raleqbi1dv c = a p c c N p p a a N p
7 4 6 bitr3id c = a r c c N r p a a N p
8 7 cbvrabv c 𝒫 X | r c c N r = a 𝒫 X | p a a 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 b a 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 X N = 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 X N p V
20 mpteqb p X N p V p X N p = p X nei j p p X N p = nei j p
21 19 20 ax-mp p X N p = p X nei j p p X N p = nei j p
22 17 21 bitrdi U UnifOn X N = p X nei j p p X N p = nei j p
23 22 reubidv U UnifOn X ∃! j TopOn X N = p X nei j p ∃! j TopOn X p X N p = nei j p
24 15 23 mpbid U UnifOn X ∃! j TopOn X p X N p = nei j p