Definition df-utop 24550

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

Assertion

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

Distinct variable group:   𝑢,𝑎,𝑣,𝑥

Detailed syntax breakdown of Definition df-utop

Step	Hyp	Ref	Expression
1		cutop 24549	. 2 class unifTop
2		vu	. . 3 setvar 𝑢
3		cust 24519	. . . . 5 class UnifOn
4	3	crn 5652	. . . 4 class ran UnifOn
5	4	cuni 4867	. . 3 class ∪ ran UnifOn
6		vv	. . . . . . . . 9 setvar 𝑣
7	6	cv 1569	. . . . . . . 8 class 𝑣
8		vx	. . . . . . . . . 10 setvar 𝑥
9	8	cv 1569	. . . . . . . . 9 class 𝑥
10	9	csn 4584	. . . . . . . 8 class {𝑥}
11	7, 10	cima 5654	. . . . . . 7 class (𝑣 “ {𝑥})
12		va	. . . . . . . 8 setvar 𝑎
13	12	cv 1569	. . . . . . 7 class 𝑎
14	11, 13	wss 3899	. . . . . 6 wff (𝑣 “ {𝑥}) ⊆ 𝑎
15	2	cv 1569	. . . . . 6 class 𝑢
16	14, 6, 15	wrex 3087	. . . . 5 wff ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
17	16, 8, 13	wral 3077	. . . 4 wff ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
18	15	cuni 4867	. . . . . 6 class ∪ 𝑢
19	18	cdm 5651	. . . . 5 class dom ∪ 𝑢
20	19	cpw 4557	. . . 4 class 𝒫 dom ∪ 𝑢
21	17, 12, 20	crab 3413	. . 3 class {𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎}
22	2, 5, 21	cmpt 5186	. 2 class (𝑢 ∈ ∪ ran UnifOn ↦ {𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
23	1, 22	wceq 1570	1 wff unifTop = (𝑢 ∈ ∪ ran UnifOn ↦ {𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})

This definition is used by:  utopval  24551