This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cust class UnifOn
1 vx setvar x
2 cvv class V
3 vu setvar u
4 3 cv setvar u
5 1 cv setvar x
6 5 5 cxp class x × x
7 6 cpw class 𝒫 x × x
8 4 7 wss wff u ⊆ 𝒫 x × x
9 6 4 wcel wff x × x ∈ u
10 vv setvar v
11 vw setvar w
12 10 cv setvar v
13 11 cv setvar w
14 12 13 wss wff v ⊆ w
15 13 4 wcel wff w ∈ u
16 14 15 wi wff v ⊆ w → w ∈ u
17 16 11 7 wral wff ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u
18 12 13 cin class v ∩ w
19 18 4 wcel wff v ∩ w ∈ u
20 19 11 4 wral wff ∀ w ∈ u v ∩ w ∈ u
21 cid class I
22 21 5 cres class I ↾ x
23 22 12 wss wff I ↾ x ⊆ v
24 12 ccnv class v -1
25 24 4 wcel wff v -1 ∈ u
26 13 13 ccom class w ∘ w
27 26 12 wss wff w ∘ w ⊆ v
28 27 11 4 wrex wff ∃ w ∈ u w ∘ w ⊆ v
29 23 25 28 w3a wff I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v
30 17 20 29 w3a wff ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v
31 30 10 4 wral wff ∀ v ∈ u ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v
32 8 9 31 w3a wff u ⊆ 𝒫 x × x ∧ x × x ∈ u ∧ ∀ v ∈ u ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v
33 32 3 cab class u | u ⊆ 𝒫 x × x ∧ x × x ∈ u ∧ ∀ v ∈ u ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v
34 1 2 33 cmpt class x ∈ V ⟼ u | u ⊆ 𝒫 x × x ∧ x × x ∈ u ∧ ∀ v ∈ u ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v
35 0 34 wceq wff UnifOn = x ∈ V ⟼ u | u ⊆ 𝒫 x × x ∧ x × x ∈ u ∧ ∀ v ∈ u ∀ w ∈ 𝒫 x × x v ⊆ w → w ∈ u ∧ ∀ w ∈ u v ∩ w ∈ u ∧ I ↾ x ⊆ v ∧ v -1 ∈ u ∧ ∃ w ∈ u w ∘ w ⊆ v