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 ‘ 𝑈 ) )