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 = u ∈ ⋃ ran ⁡ UnifOn ⟼ a ∈ 𝒫 dom ⁡ ⋃ u | ∀ x ∈ a ∃ v ∈ u v x ⊆ a

Detailed syntax breakdown

Step Hyp Ref Expression
0 cutop class unifTop
1 vu setvar u
2 cust class UnifOn
3 2 crn class ran ⁡ UnifOn
4 3 cuni class ⋃ ran ⁡ UnifOn
5 va setvar a
6 1 cv setvar u
7 6 cuni class ⋃ u
8 7 cdm class dom ⁡ ⋃ u
9 8 cpw class 𝒫 dom ⁡ ⋃ u
10 vx setvar x
11 5 cv setvar a
12 vv setvar v
13 12 cv setvar v
14 10 cv setvar x
15 14 csn class x
16 13 15 cima class v x
17 16 11 wss wff v x ⊆ a
18 17 12 6 wrex wff ∃ v ∈ u v x ⊆ a
19 18 10 11 wral wff ∀ x ∈ a ∃ v ∈ u v x ⊆ a
20 19 5 9 crab class a ∈ 𝒫 dom ⁡ ⋃ u | ∀ x ∈ a ∃ v ∈ u v x ⊆ a
21 1 4 20 cmpt class u ∈ ⋃ ran ⁡ UnifOn ⟼ a ∈ 𝒫 dom ⁡ ⋃ u | ∀ x ∈ a ∃ v ∈ u v x ⊆ a
22 0 21 wceq wff unifTop = u ∈ ⋃ ran ⁡ UnifOn ⟼ a ∈ 𝒫 dom ⁡ ⋃ u | ∀ x ∈ a ∃ v ∈ u v x ⊆ a