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∈Uvx⊆a
2 ssrab2 ⊢a∈𝒫X|∀x∈a∃v∈Uvx⊆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 ⊢vx⊆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→vx⊆X
11 5 10 syl ⊢U∈UnifOn⁡X∧v∈U→vx⊆X
12 11 ralrimiva ⊢U∈UnifOn⁡X→∀v∈Uvx⊆X
13 ustne0 ⊢U∈UnifOn⁡X→U≠∅
14 r19.2zb ⊢U≠∅↔∀v∈Uvx⊆X→∃v∈Uvx⊆X
15 13 14 sylib ⊢U∈UnifOn⁡X→∀v∈Uvx⊆X→∃v∈Uvx⊆X
16 12 15 mpd ⊢U∈UnifOn⁡X→∃v∈Uvx⊆X
17 16 ralrimivw ⊢U∈UnifOn⁡X→∀x∈X∃v∈Uvx⊆X
18 elutop ⊢U∈UnifOn⁡X→X∈unifTop⁡U↔X⊆X∧∀x∈X∃v∈Uvx⊆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