Definition df-ust 23352

Description: Definition of a uniform structure. Definition 1 of [BourbakiTop1] p. II.1. A uniform structure is used to give a generalization of the idea of Cauchy's sequence. This definition is analogous to TopOn. Elements of an uniform structure are called entourages. (Contributed by FL, 29-May-2014.) (Revised by Thierry Arnoux, 15-Nov-2017.)

Assertion

Ref	Expression
df-ust	⊢ UnifOn = (𝑥 ∈ V ↦ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})

Distinct variable group:   𝑥,𝑢,𝑣,𝑤

Detailed syntax breakdown of Definition df-ust

Step	Hyp	Ref	Expression
1		cust 23351	. 2 class UnifOn
2		vx	. . 3 setvar 𝑥
3		cvv 3432	. . 3 class V
4		vu	. . . . . . 7 setvar 𝑢
5	4	cv 1538	. . . . . 6 class 𝑢
6	2	cv 1538	. . . . . . . 8 class 𝑥
7	6, 6	cxp 5587	. . . . . . 7 class (𝑥 × 𝑥)
8	7	cpw 4533	. . . . . 6 class 𝒫 (𝑥 × 𝑥)
9	5, 8	wss 3887	. . . . 5 wff 𝑢 ⊆ 𝒫 (𝑥 × 𝑥)
10	7, 5	wcel 2106	. . . . 5 wff (𝑥 × 𝑥) ∈ 𝑢
11		vv	. . . . . . . . . . 11 setvar 𝑣
12	11	cv 1538	. . . . . . . . . 10 class 𝑣
13		vw	. . . . . . . . . . 11 setvar 𝑤
14	13	cv 1538	. . . . . . . . . 10 class 𝑤
15	12, 14	wss 3887	. . . . . . . . 9 wff 𝑣 ⊆ 𝑤
16	13, 4	wel 2107	. . . . . . . . 9 wff 𝑤 ∈ 𝑢
17	15, 16	wi 4	. . . . . . . 8 wff (𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢)
18	17, 13, 8	wral 3064	. . . . . . 7 wff ∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢)
19	12, 14	cin 3886	. . . . . . . . 9 class (𝑣 ∩ 𝑤)
20	19, 5	wcel 2106	. . . . . . . 8 wff (𝑣 ∩ 𝑤) ∈ 𝑢
21	20, 13, 5	wral 3064	. . . . . . 7 wff ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢
22		cid 5488	. . . . . . . . . 10 class I
23	22, 6	cres 5591	. . . . . . . . 9 class ( I ↾ 𝑥)
24	23, 12	wss 3887	. . . . . . . 8 wff ( I ↾ 𝑥) ⊆ 𝑣
25	12	ccnv 5588	. . . . . . . . 9 class ◡𝑣
26	25, 5	wcel 2106	. . . . . . . 8 wff ◡𝑣 ∈ 𝑢
27	14, 14	ccom 5593	. . . . . . . . . 10 class (𝑤 ∘ 𝑤)
28	27, 12	wss 3887	. . . . . . . . 9 wff (𝑤 ∘ 𝑤) ⊆ 𝑣
29	28, 13, 5	wrex 3065	. . . . . . . 8 wff ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣
30	24, 26, 29	w3a 1086	. . . . . . 7 wff (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)
31	18, 21, 30	w3a 1086	. . . . . 6 wff (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣))
32	31, 11, 5	wral 3064	. . . . 5 wff ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣))
33	9, 10, 32	w3a 1086	. . . 4 wff (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))
34	33, 4	cab 2715	. . 3 class {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))}
35	2, 3, 34	cmpt 5157	. 2 class (𝑥 ∈ V ↦ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})
36	1, 35	wceq 1539	1 wff UnifOn = (𝑥 ∈ V ↦ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))})

This definition is referenced by:  ustfn  23353  ustval  23354  ustn0  23372