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