ustexsym

Description: In an uniform structure, for any entourage V , there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018)

		Ref	Expression
	Assertion	ustexsym	$⊢ (U \in UnifOn (X) \land V \in U) \to \exists w \in U (w^{-1} = w \land w \subseteq V)$

Proof

Step	Hyp	Ref	Expression
1		simplll	$⊢ (((U \in UnifOn (X) \land V \in U) \land x \in U) \land x \circ x \subseteq V) \to U \in UnifOn (X)$
2		ustinvel	$⊢ (U \in UnifOn (X) \land x \in U) \to x^{-1} \in U$
3	2	ad4ant13	$⊢ (((U \in UnifOn (X) \land V \in U) \land x \in U) \land x \circ x \subseteq V) \to x^{-1} \in U$
4		simplr	$⊢ (((U \in UnifOn (X) \land V \in U) \land x \in U) \land x \circ x \subseteq V) \to x \in U$
5		ustincl	$⊢ (U \in UnifOn (X) \land x^{-1} \in U \land x \in U) \to x^{-1} \cap x \in U$
6	1 3 4 5	syl3anc	$⊢ (((U \in UnifOn (X) \land V \in U) \land x \in U) \land x \circ x \subseteq V) \to x^{-1} \cap x \in U$
7		ustrel	$⊢ (U \in UnifOn (X) \land x \in U) \to Rel x$
8		dfrel2	$⊢ Rel x \leftrightarrow {x^{-1}}^{-1} = x$
9	7 8	sylib	$⊢ (U \in UnifOn (X) \land x \in U) \to {x^{-1}}^{-1} = x$
10	9	ineq1d	$⊢ (U \in UnifOn (X) \land x \in U) \to {x^{-1}}^{-1} \cap x^{-1} = x \cap x^{-1}$
11		cnvin	$⊢ {(x^{-1} \cap x)}^{-1} = {x^{-1}}^{-1} \cap x^{-1}$
12		incom	$⊢ x^{-1} \cap x = x \cap x^{-1}$
13	10 11 12	3eqtr4g	$⊢ (U \in UnifOn (X) \land x \in U) \to {(x^{-1} \cap x)}^{-1} = x^{-1} \cap x$
14	13	ad4ant13	$⊢ (((U \in UnifOn (X) \land V \in U) \land x \in U) \land x \circ x \subseteq V) \to {(x^{-1} \cap x)}^{-1} = x^{-1} \cap x$
15		inss2	$⊢ x^{-1} \cap x \subseteq x$
16		ustssco	$⊢ (U \in UnifOn (X) \land x \in U) \to x \subseteq x \circ x$
17	16	ad4ant13	$⊢ (((U \in UnifOn (X) \land V \in U) \land x \in U) \land x \circ x \subseteq V) \to x \subseteq x \circ x$
18		simpr	$⊢ (((U \in UnifOn (X) \land V \in U) \land x \in U) \land x \circ x \subseteq V) \to x \circ x \subseteq V$
19	17 18	sstrd	$⊢ (((U \in UnifOn (X) \land V \in U) \land x \in U) \land x \circ x \subseteq V) \to x \subseteq V$
20	15 19	sstrid	$⊢ (((U \in UnifOn (X) \land V \in U) \land x \in U) \land x \circ x \subseteq V) \to x^{-1} \cap x \subseteq V$
21		cnveq	$⊢ w = x^{-1} \cap x \to w^{-1} = {(x^{-1} \cap x)}^{-1}$
22		id	$⊢ w = x^{-1} \cap x \to w = x^{-1} \cap x$
23	21 22	eqeq12d	$⊢ w = x^{-1} \cap x \to (w^{-1} = w \leftrightarrow {(x^{-1} \cap x)}^{-1} = x^{-1} \cap x)$
24		sseq1	$⊢ w = x^{-1} \cap x \to (w \subseteq V \leftrightarrow x^{-1} \cap x \subseteq V)$
25	23 24	anbi12d	$⊢ w = x^{-1} \cap x \to ((w^{-1} = w \land w \subseteq V) \leftrightarrow ({(x^{-1} \cap x)}^{-1} = x^{-1} \cap x \land x^{-1} \cap x \subseteq V))$
26	25	rspcev	$⊢ (x^{-1} \cap x \in U \land ({(x^{-1} \cap x)}^{-1} = x^{-1} \cap x \land x^{-1} \cap x \subseteq V)) \to \exists w \in U (w^{-1} = w \land w \subseteq V)$
27	6 14 20 26	syl12anc	$⊢ (((U \in UnifOn (X) \land V \in U) \land x \in U) \land x \circ x \subseteq V) \to \exists w \in U (w^{-1} = w \land w \subseteq V)$
28		ustexhalf	$⊢ (U \in UnifOn (X) \land V \in U) \to \exists x \in U x \circ x \subseteq V$
29	27 28	r19.29a	$⊢ (U \in UnifOn (X) \land V \in U) \to \exists w \in U (w^{-1} = w \land w \subseteq V)$

Metamath Proof Explorer

Theorem ustexsym

Proof