Metamath Proof Explorer

Theorem utopbas

Description: The base of the topology induced by a uniform structure U . (Contributed by Thierry Arnoux, 5-Dec-2017)

Ref Expression
Assertion utopbas ⊢ U ∈ UnifOn ⁡ X → X = ⋃ unifTop ⁡ U

Proof

Step Hyp Ref Expression
1 utopval ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U = a ∈ 𝒫 X | ∀ x ∈ a ∃ v ∈ U v x ⊆ a
2 ssrab2 ⊢ a ∈ 𝒫 X | ∀ x ∈ a ∃ v ∈ U v x ⊆ a ⊆ 𝒫 X
3 1 2 eqsstrdi ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U ⊆ 𝒫 X
4 ssidd ⊢ U ∈ UnifOn ⁡ X → X ⊆ X
5 ustssxp ⊢ U ∈ UnifOn ⁡ X ∧ v ∈ U → v ⊆ X × X
6 imassrn ⊢ v x ⊆ ran ⁡ v
7 rnss ⊢ v ⊆ X × X → ran ⁡ v ⊆ ran ⁡ X × X
8 rnxpid ⊢ ran ⁡ X × X = X
9 7 8 sseqtrdi ⊢ v ⊆ X × X → ran ⁡ v ⊆ X
10 6 9 sstrid ⊢ v ⊆ X × X → v x ⊆ X
11 5 10 syl ⊢ U ∈ UnifOn ⁡ X ∧ v ∈ U → v x ⊆ X
12 11 ralrimiva ⊢ U ∈ UnifOn ⁡ X → ∀ v ∈ U v x ⊆ X
13 ustne0 ⊢ U ∈ UnifOn ⁡ X → U ≠ ∅
14 r19.2zb ⊢ U ≠ ∅ ↔ ∀ v ∈ U v x ⊆ X → ∃ v ∈ U v x ⊆ X
15 13 14 sylib ⊢ U ∈ UnifOn ⁡ X → ∀ v ∈ U v x ⊆ X → ∃ v ∈ U v x ⊆ X
16 12 15 mpd ⊢ U ∈ UnifOn ⁡ X → ∃ v ∈ U v x ⊆ X
17 16 ralrimivw ⊢ U ∈ UnifOn ⁡ X → ∀ x ∈ X ∃ v ∈ U v x ⊆ X
18 elutop ⊢ U ∈ UnifOn ⁡ X → X ∈ unifTop ⁡ U ↔ X ⊆ X ∧ ∀ x ∈ X ∃ v ∈ U v x ⊆ X
19 4 17 18 mpbir2and ⊢ U ∈ UnifOn ⁡ X → X ∈ unifTop ⁡ U
20 elpwuni ⊢ X ∈ unifTop ⁡ U → unifTop ⁡ U ⊆ 𝒫 X ↔ ⋃ unifTop ⁡ U = X
21 19 20 syl ⊢ U ∈ UnifOn ⁡ X → unifTop ⁡ U ⊆ 𝒫 X ↔ ⋃ unifTop ⁡ U = X
22 3 21 mpbid ⊢ U ∈ UnifOn ⁡ X → ⋃ unifTop ⁡ U = X
23 22 eqcomd ⊢ U ∈ UnifOn ⁡ X → X = ⋃ unifTop ⁡ U