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

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 ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ∪ ( unifTop ‘ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 utopval ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )
2 ssrab2 ⊢ { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } ⊆ 𝒫 𝑋
3 1 2 eqsstrdi ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ⊆ 𝒫 𝑋 )
4 ssidd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ⊆ 𝑋 )
5 ustssxp ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → 𝑣 ⊆ ( 𝑋 × 𝑋 ) )
6 imassrn ⊢ ( 𝑣 “ { 𝑥 } ) ⊆ ran 𝑣
7 rnss ⊢ ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) → ran 𝑣 ⊆ ran ( 𝑋 × 𝑋 ) )
8 rnxpid ⊢ ran ( 𝑋 × 𝑋 ) = 𝑋
9 7 8 sseqtrdi ⊢ ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) → ran 𝑣 ⊆ 𝑋 )
10 6 9 sstrid ⊢ ( 𝑣 ⊆ ( 𝑋 × 𝑋 ) → ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 )
11 5 10 syl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 )
12 11 ralrimiva ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∀ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 )
13 ustne0 ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ≠ ∅ )
14 r19.2zb ⊢ ( 𝑈 ≠ ∅ ↔ ( ∀ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 ) )
15 13 14 sylib ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ∀ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 ) )
16 12 15 mpd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 )
17 16 ralrimivw ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 )
18 elutop ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 ∈ ( unifTop ‘ 𝑈 ) ↔ ( 𝑋 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑣 ∈ 𝑈 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑋 ) ) )
19 4 17 18 mpbir2and ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ∈ ( unifTop ‘ 𝑈 ) )
20 elpwuni ⊢ ( 𝑋 ∈ ( unifTop ‘ 𝑈 ) → ( ( unifTop ‘ 𝑈 ) ⊆ 𝒫 𝑋 ↔ ∪ ( unifTop ‘ 𝑈 ) = 𝑋 ) )
21 19 20 syl ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( unifTop ‘ 𝑈 ) ⊆ 𝒫 𝑋 ↔ ∪ ( unifTop ‘ 𝑈 ) = 𝑋 ) )
22 3 21 mpbid ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ ( unifTop ‘ 𝑈 ) = 𝑋 )
23 22 eqcomd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ∪ ( unifTop ‘ 𝑈 ) )