Metamath Proof Explorer

Definition df-ust

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)

Ref Expression
Assertion df-ust ⊢UnifOn=x∈V⟼u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cust classUnifOn
1 vx setvarx
2 cvv classV
3 vu setvaru
4 3 cv setvaru
5 1 cv setvarx
6 5 5 cxp classx×x
7 6 cpw class𝒫x×x
8 4 7 wss wffu⊆𝒫x×x
9 6 4 wcel wffx×x∈u
10 vv setvarv
11 vw setvarw
12 10 cv setvarv
13 11 cv setvarw
14 12 13 wss wffv⊆w
15 13 4 wcel wffw∈u
16 14 15 wi wffv⊆w→w∈u
17 16 11 7 wral wff∀w∈𝒫x×xv⊆w→w∈u
18 12 13 cin classv∩w
19 18 4 wcel wffv∩w∈u
20 19 11 4 wral wff∀w∈uv∩w∈u
21 cid classI
22 21 5 cres classI↾x
23 22 12 wss wffI↾x⊆v
24 12 ccnv classv-1
25 24 4 wcel wffv-1∈u
26 13 13 ccom classw∘w
27 26 12 wss wffw∘w⊆v
28 27 11 4 wrex wff∃w∈uw∘w⊆v
29 23 25 28 w3a wffI↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v
30 17 20 29 w3a wff∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v
31 30 10 4 wral wff∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v
32 8 9 31 w3a wffu⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v
33 32 3 cab classu|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v
34 1 2 33 cmpt classx∈V⟼u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v
35 0 34 wceq wffUnifOn=x∈V⟼u|u⊆𝒫x×x∧x×x∈u∧∀v∈u∀w∈𝒫x×xv⊆w→w∈u∧∀w∈uv∩w∈u∧I↾x⊆v∧v-1∈u∧∃w∈uw∘w⊆v