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