This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )

Proof

Step Hyp Ref Expression
1 df-utop ⊢ unifTop = ( 𝑢 ∈ ∪ ran UnifOn ↦ { 𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )
2 simpr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → 𝑢 = 𝑈 )
3 2 unieqd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ∪ 𝑢 = ∪ 𝑈 )
4 3 dmeqd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → dom ∪ 𝑢 = dom ∪ 𝑈 )
5 ustbas2 ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = dom ∪ 𝑈 )
6 5 adantr ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → 𝑋 = dom ∪ 𝑈 )
7 4 6 eqtr4d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → dom ∪ 𝑢 = 𝑋 )
8 7 pweqd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → 𝒫 dom ∪ 𝑢 = 𝒫 𝑋 )
9 2 rexeqdv ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ( ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) )
10 9 ralbidv ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → ( ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ↔ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 ) )
11 8 10 rabeqbidv ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑢 = 𝑈 ) → { 𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )
12 elfvunirn ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ∈ ∪ ran UnifOn )
13 elfvex ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ∈ V )
14 pwexg ⊢ ( 𝑋 ∈ V → 𝒫 𝑋 ∈ V )
15 rabexg ⊢ ( 𝒫 𝑋 ∈ V → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } ∈ V )
16 13 14 15 3syl ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } ∈ V )
17 1 11 12 16 fvmptd2 ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )