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 elrnust 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