Metamath Proof Explorer


Definition df-utop

Description: Definition of a topology induced by a uniform structure. Definition 3 of BourbakiTop1 p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017)

Ref Expression
Assertion df-utop unifTop = ( 𝑢 ran UnifOn ↦ { 𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀ 𝑥𝑎𝑣𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cutop unifTop
1 vu 𝑢
2 cust UnifOn
3 2 crn ran UnifOn
4 3 cuni ran UnifOn
5 va 𝑎
6 1 cv 𝑢
7 6 cuni 𝑢
8 7 cdm dom 𝑢
9 8 cpw 𝒫 dom 𝑢
10 vx 𝑥
11 5 cv 𝑎
12 vv 𝑣
13 12 cv 𝑣
14 10 cv 𝑥
15 14 csn { 𝑥 }
16 13 15 cima ( 𝑣 “ { 𝑥 } )
17 16 11 wss ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎
18 17 12 6 wrex 𝑣𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎
19 18 10 11 wral 𝑥𝑎𝑣𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎
20 19 5 9 crab { 𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀ 𝑥𝑎𝑣𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 }
21 1 4 20 cmpt ( 𝑢 ran UnifOn ↦ { 𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀ 𝑥𝑎𝑣𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )
22 0 21 wceq unifTop = ( 𝑢 ran UnifOn ↦ { 𝑎 ∈ 𝒫 dom 𝑢 ∣ ∀ 𝑥𝑎𝑣𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )