MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ust Structured version   Visualization version   GIF version

Definition df-ust 21814
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
StepHypRef Expression
1 cust 21813 . 2 class UnifOn
2 vx . . 3 setvar 𝑥
3 cvv 3173 . . 3 class V
4 vu . . . . . . 7 setvar 𝑢
54cv 1474 . . . . . 6 class 𝑢
62cv 1474 . . . . . . . 8 class 𝑥
76, 6cxp 5036 . . . . . . 7 class (𝑥 × 𝑥)
87cpw 4108 . . . . . 6 class 𝒫 (𝑥 × 𝑥)
95, 8wss 3540 . . . . 5 wff 𝑢 ⊆ 𝒫 (𝑥 × 𝑥)
107, 5wcel 1977 . . . . 5 wff (𝑥 × 𝑥) ∈ 𝑢
11 vv . . . . . . . . . . 11 setvar 𝑣
1211cv 1474 . . . . . . . . . 10 class 𝑣
13 vw . . . . . . . . . . 11 setvar 𝑤
1413cv 1474 . . . . . . . . . 10 class 𝑤
1512, 14wss 3540 . . . . . . . . 9 wff 𝑣𝑤
1613, 4wel 1978 . . . . . . . . 9 wff 𝑤𝑢
1715, 16wi 4 . . . . . . . 8 wff (𝑣𝑤𝑤𝑢)
1817, 13, 8wral 2896 . . . . . . 7 wff 𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢)
1912, 14cin 3539 . . . . . . . . 9 class (𝑣𝑤)
2019, 5wcel 1977 . . . . . . . 8 wff (𝑣𝑤) ∈ 𝑢
2120, 13, 5wral 2896 . . . . . . 7 wff 𝑤𝑢 (𝑣𝑤) ∈ 𝑢
22 cid 4948 . . . . . . . . . 10 class I
2322, 6cres 5040 . . . . . . . . 9 class ( I ↾ 𝑥)
2423, 12wss 3540 . . . . . . . 8 wff ( I ↾ 𝑥) ⊆ 𝑣
2512ccnv 5037 . . . . . . . . 9 class 𝑣
2625, 5wcel 1977 . . . . . . . 8 wff 𝑣𝑢
2714, 14ccom 5042 . . . . . . . . . 10 class (𝑤𝑤)
2827, 12wss 3540 . . . . . . . . 9 wff (𝑤𝑤) ⊆ 𝑣
2928, 13, 5wrex 2897 . . . . . . . 8 wff 𝑤𝑢 (𝑤𝑤) ⊆ 𝑣
3024, 26, 29w3a 1031 . . . . . . 7 wff (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣)
3118, 21, 30w3a 1031 . . . . . 6 wff (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣))
3231, 11, 5wral 2896 . . . . 5 wff 𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣))
339, 10, 32w3a 1031 . . . 4 wff (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣)))
3433, 4cab 2596 . . 3 class {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣)))}
352, 3, 34cmpt 4643 . 2 class (𝑥 ∈ V ↦ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣)))})
361, 35wceq 1475 1 wff UnifOn = (𝑥 ∈ V ↦ {𝑢 ∣ (𝑢 ⊆ 𝒫 (𝑥 × 𝑥) ∧ (𝑥 × 𝑥) ∈ 𝑢 ∧ ∀𝑣𝑢 (∀𝑤 ∈ 𝒫 (𝑥 × 𝑥)(𝑣𝑤𝑤𝑢) ∧ ∀𝑤𝑢 (𝑣𝑤) ∈ 𝑢 ∧ (( I ↾ 𝑥) ⊆ 𝑣𝑣𝑢 ∧ ∃𝑤𝑢 (𝑤𝑤) ⊆ 𝑣)))})
Colors of variables: wff setvar class
This definition is referenced by:  ustfn  21815  ustval  21816  ustn0  21834
  Copyright terms: Public domain W3C validator