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 = ( 𝑥 ∈ V ↦ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cust ⊢ UnifOn
1 vx ⊢ 𝑥
2 cvv ⊢ V
3 vu ⊢ 𝑢
4 3 cv ⊢ 𝑢
5 1 cv ⊢ 𝑥
6 5 5 cxp ⊢ ( 𝑥 × 𝑥 )
7 6 cpw ⊢ 𝒫 ( 𝑥 × 𝑥 )
8 4 7 wss ⊢ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 )
9 6 4 wcel ⊢ ( 𝑥 × 𝑥 ) ∈ 𝑢
10 vv ⊢ 𝑣
11 vw ⊢ 𝑤
12 10 cv ⊢ 𝑣
13 11 cv ⊢ 𝑤
14 12 13 wss ⊢ 𝑣 ⊆ 𝑤
15 13 4 wcel ⊢ 𝑤 ∈ 𝑢
16 14 15 wi ⊢ ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 )
17 16 11 7 wral ⊢ ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 )
18 12 13 cin ⊢ ( 𝑣 ∩ 𝑤 )
19 18 4 wcel ⊢ ( 𝑣 ∩ 𝑤 ) ∈ 𝑢
20 19 11 4 wral ⊢ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢
21 cid ⊢ I
22 21 5 cres ⊢ ( I ↾ 𝑥 )
23 22 12 wss ⊢ ( I ↾ 𝑥 ) ⊆ 𝑣
24 12 ccnv ⊢ ◡ 𝑣
25 24 4 wcel ⊢ ◡ 𝑣 ∈ 𝑢
26 13 13 ccom ⊢ ( 𝑤 ∘ 𝑤 )
27 26 12 wss ⊢ ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣
28 27 11 4 wrex ⊢ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣
29 23 25 28 w3a ⊢ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 )
30 17 20 29 w3a ⊢ ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) )
31 30 10 4 wral ⊢ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) )
32 8 9 31 w3a ⊢ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) )
33 32 3 cab ⊢ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) }
34 1 2 33 cmpt ⊢ ( 𝑥 ∈ V ↦ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } )
35 0 34 wceq ⊢ UnifOn = ( 𝑥 ∈ V ↦ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } )