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

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 ∪ 𝑢 ∣ ∀ 𝑥 ∈ 𝑎 ∃ 𝑣 ∈ 𝑢 ( 𝑣 “ { 𝑥 } ) ⊆ 𝑎 } )