Definition df-utop 21845

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 21844	. 2 class unifTop
2		vu	. . 3 setvar 𝑢
3		cust 21813	. . . . 5 class UnifOn
4	3	crn 5039	. . . 4 class ran UnifOn
5	4	cuni 4372	. . 3 class ∪ ran UnifOn
6		vv	. . . . . . . . 9 setvar 𝑣
7	6	cv 1474	. . . . . . . 8 class 𝑣
8		vx	. . . . . . . . . 10 setvar 𝑥
9	8	cv 1474	. . . . . . . . 9 class 𝑥
10	9	csn 4125	. . . . . . . 8 class {𝑥}
11	7, 10	cima 5041	. . . . . . 7 class (𝑣 “ {𝑥})
12		va	. . . . . . . 8 setvar 𝑎
13	12	cv 1474	. . . . . . 7 class 𝑎
14	11, 13	wss 3540	. . . . . 6 wff (𝑣 “ {𝑥}) ⊆ 𝑎
15	2	cv 1474	. . . . . 6 class 𝑢
16	14, 6, 15	wrex 2897	. . . . 5 wff ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
17	16, 8, 13	wral 2896	. . . 4 wff ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎
18	15	cuni 4372	. . . . . 6 class ∪ 𝑢
19	18	cdm 5038	. . . . 5 class dom ∪ 𝑢
20	19	cpw 4108	. . . 4 class 𝒫 dom ∪ 𝑢
21	17, 12, 20	crab 2900	. . 3 class {𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎}
22	2, 5, 21	cmpt 4643	. 2 class (𝑢 ∈ ∪ ran UnifOn ↦ {𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})
23	1, 22	wceq 1475	1 wff unifTop = (𝑢 ∈ ∪ ran UnifOn ↦ {𝑎 ∈ 𝒫 dom ∪ 𝑢 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑢 (𝑣 “ {𝑥}) ⊆ 𝑎})

This definition is referenced by:  utopval  21846