Metamath Proof Explorer

Theorem utopval

Description: The topology induced by a uniform structure U . (Contributed by Thierry Arnoux, 30-Nov-2017)

Ref Expression
Assertion utopval ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U = a ∈ 𝒫 X | ∀ x ∈ a ∃ v ∈ U v x ⊆ a

Proof

Step Hyp Ref Expression
1 df-utop ⊢ unifTop = u ∈ ⋃ ran ⁡ UnifOn ⟼ a ∈ 𝒫 dom ⁡ ⋃ u | ∀ x ∈ a ∃ v ∈ u v x ⊆ a
2 simpr ⊢ U ∈ UnifOn ⁡ X ∧ u = U → u = U
3 2 unieqd ⊢ U ∈ UnifOn ⁡ X ∧ u = U → ⋃ u = ⋃ U
4 3 dmeqd ⊢ U ∈ UnifOn ⁡ X ∧ u = U → dom ⁡ ⋃ u = dom ⁡ ⋃ U
5 ustbas2 ⊢ U ∈ UnifOn ⁡ X → X = dom ⁡ ⋃ U
6 5 adantr ⊢ U ∈ UnifOn ⁡ X ∧ u = U → X = dom ⁡ ⋃ U
7 4 6 eqtr4d ⊢ U ∈ UnifOn ⁡ X ∧ u = U → dom ⁡ ⋃ u = X
8 7 pweqd ⊢ U ∈ UnifOn ⁡ X ∧ u = U → 𝒫 dom ⁡ ⋃ u = 𝒫 X
9 2 rexeqdv ⊢ U ∈ UnifOn ⁡ X ∧ u = U → ∃ v ∈ u v x ⊆ a ↔ ∃ v ∈ U v x ⊆ a
10 9 ralbidv ⊢ U ∈ UnifOn ⁡ X ∧ u = U → ∀ x ∈ a ∃ v ∈ u v x ⊆ a ↔ ∀ x ∈ a ∃ v ∈ U v x ⊆ a
11 8 10 rabeqbidv ⊢ U ∈ UnifOn ⁡ X ∧ u = U → a ∈ 𝒫 dom ⁡ ⋃ u | ∀ x ∈ a ∃ v ∈ u v x ⊆ a = a ∈ 𝒫 X | ∀ x ∈ a ∃ v ∈ U v x ⊆ a
12 elfvunirn ⊢ U ∈ UnifOn ⁡ X → U ∈ ⋃ ran ⁡ UnifOn
13 elfvex ⊢ U ∈ UnifOn ⁡ X → X ∈ V
14 pwexg ⊢ X ∈ V → 𝒫 X ∈ V
15 rabexg ⊢ 𝒫 X ∈ V → a ∈ 𝒫 X | ∀ x ∈ a ∃ v ∈ U v x ⊆ a ∈ V
16 13 14 15 3syl ⊢ U ∈ UnifOn ⁡ X → a ∈ 𝒫 X | ∀ x ∈ a ∃ v ∈ U v x ⊆ a ∈ V
17 1 11 12 16 fvmptd2 ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U = a ∈ 𝒫 X | ∀ x ∈ a ∃ v ∈ U v x ⊆ a