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 \in V ⟼ \{u \| (u \subseteq 𝒫 (x \times x) \land x \times x \in u \land \forall v \in u (\forall w \in 𝒫 (x \times x) (v \subseteq w \to w \in u) \land \forall w \in u v \cap w \in u \land ({I ↾}_{x} \subseteq v \land v^{-1} \in u \land \exists w \in u w \circ w \subseteq 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 \times x)$
7	6	cpw	$class 𝒫 (x \times x)$
8	4 7	wss	$wff u \subseteq 𝒫 (x \times x)$
9	6 4	wcel	$wff x \times x \in 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 \subseteq w$
15	13 4	wcel	$wff w \in u$
16	14 15	wi	$wff (v \subseteq w \to w \in u)$
17	16 11 7	wral	$wff \forall w \in 𝒫 (x \times x) (v \subseteq w \to w \in u)$
18	12 13	cin	$class (v \cap w)$
19	18 4	wcel	$wff v \cap w \in u$
20	19 11 4	wral	$wff \forall w \in u v \cap w \in u$
21		cid	$class I$
22	21 5	cres	$class ({I ↾}_{x})$
23	22 12	wss	$wff {I ↾}_{x} \subseteq v$
24	12	ccnv	$class v^{-1}$
25	24 4	wcel	$wff v^{-1} \in u$
26	13 13	ccom	$class (w \circ w)$
27	26 12	wss	$wff w \circ w \subseteq v$
28	27 11 4	wrex	$wff \exists w \in u w \circ w \subseteq v$
29	23 25 28	w3a	$wff ({I ↾}_{x} \subseteq v \land v^{-1} \in u \land \exists w \in u w \circ w \subseteq v)$
30	17 20 29	w3a	$wff (\forall w \in 𝒫 (x \times x) (v \subseteq w \to w \in u) \land \forall w \in u v \cap w \in u \land ({I ↾}_{x} \subseteq v \land v^{-1} \in u \land \exists w \in u w \circ w \subseteq v))$
31	30 10 4	wral	$wff \forall v \in u (\forall w \in 𝒫 (x \times x) (v \subseteq w \to w \in u) \land \forall w \in u v \cap w \in u \land ({I ↾}_{x} \subseteq v \land v^{-1} \in u \land \exists w \in u w \circ w \subseteq v))$
32	8 9 31	w3a	$wff (u \subseteq 𝒫 (x \times x) \land x \times x \in u \land \forall v \in u (\forall w \in 𝒫 (x \times x) (v \subseteq w \to w \in u) \land \forall w \in u v \cap w \in u \land ({I ↾}_{x} \subseteq v \land v^{-1} \in u \land \exists w \in u w \circ w \subseteq v)))$
33	32 3	cab	$class \{u \| (u \subseteq 𝒫 (x \times x) \land x \times x \in u \land \forall v \in u (\forall w \in 𝒫 (x \times x) (v \subseteq w \to w \in u) \land \forall w \in u v \cap w \in u \land ({I ↾}_{x} \subseteq v \land v^{-1} \in u \land \exists w \in u w \circ w \subseteq v)))\}$
34	1 2 33	cmpt	$class (x \in V ⟼ \{u \| (u \subseteq 𝒫 (x \times x) \land x \times x \in u \land \forall v \in u (\forall w \in 𝒫 (x \times x) (v \subseteq w \to w \in u) \land \forall w \in u v \cap w \in u \land ({I ↾}_{x} \subseteq v \land v^{-1} \in u \land \exists w \in u w \circ w \subseteq v)))\})$
35	0 34	wceq	$wff UnifOn = (x \in V ⟼ \{u \| (u \subseteq 𝒫 (x \times x) \land x \times x \in u \land \forall v \in u (\forall w \in 𝒫 (x \times x) (v \subseteq w \to w \in u) \land \forall w \in u v \cap w \in u \land ({I ↾}_{x} \subseteq v \land v^{-1} \in u \land \exists w \in u w \circ w \subseteq v)))\})$

Metamath Proof Explorer

Definition df-ust

Detailed syntax breakdown