Metamath Proof Explorer

Theorem ustex2sym

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

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

Proof

Step	Hyp	Ref	Expression
1		ustexsym	$⊢ (U \in UnifOn (X) \land v \in U) \to \exists w \in U (w^{-1} = w \land w \subseteq v)$
2	1	ad4ant13	$⊢ (((U \in UnifOn (X) \land V \in U) \land v \in U) \land v \circ v \subseteq V) \to \exists w \in U (w^{-1} = w \land w \subseteq v)$
3		simprl	$⊢ (((((U \in UnifOn (X) \land V \in U) \land v \in U) \land v \circ v \subseteq V) \land w \in U) \land (w^{-1} = w \land w \subseteq v)) \to w^{-1} = w$
4		coss1	$⊢ w \subseteq v \to w \circ w \subseteq v \circ w$
5		coss2	$⊢ w \subseteq v \to v \circ w \subseteq v \circ v$
6	4 5	sstrd	$⊢ w \subseteq v \to w \circ w \subseteq v \circ v$
7	6	ad2antll	$⊢ (((((U \in UnifOn (X) \land V \in U) \land v \in U) \land v \circ v \subseteq V) \land w \in U) \land (w^{-1} = w \land w \subseteq v)) \to w \circ w \subseteq v \circ v$
8		simpllr	$⊢ (((((U \in UnifOn (X) \land V \in U) \land v \in U) \land v \circ v \subseteq V) \land w \in U) \land (w^{-1} = w \land w \subseteq v)) \to v \circ v \subseteq V$
9	7 8	sstrd	$⊢ (((((U \in UnifOn (X) \land V \in U) \land v \in U) \land v \circ v \subseteq V) \land w \in U) \land (w^{-1} = w \land w \subseteq v)) \to w \circ w \subseteq V$
10	3 9	jca	$⊢ (((((U \in UnifOn (X) \land V \in U) \land v \in U) \land v \circ v \subseteq V) \land w \in U) \land (w^{-1} = w \land w \subseteq v)) \to (w^{-1} = w \land w \circ w \subseteq V)$
11	10	ex	$⊢ ((((U \in UnifOn (X) \land V \in U) \land v \in U) \land v \circ v \subseteq V) \land w \in U) \to ((w^{-1} = w \land w \subseteq v) \to (w^{-1} = w \land w \circ w \subseteq V))$
12	11	reximdva	$⊢ (((U \in UnifOn (X) \land V \in U) \land v \in U) \land v \circ v \subseteq V) \to (\exists w \in U (w^{-1} = w \land w \subseteq v) \to \exists w \in U (w^{-1} = w \land w \circ w \subseteq V))$
13	2 12	mpd	$⊢ (((U \in UnifOn (X) \land V \in U) \land v \in U) \land v \circ v \subseteq V) \to \exists w \in U (w^{-1} = w \land w \circ w \subseteq V)$
14		ustexhalf	$⊢ (U \in UnifOn (X) \land V \in U) \to \exists v \in U v \circ v \subseteq V$
15	13 14	r19.29a	$⊢ (U \in UnifOn (X) \land V \in U) \to \exists w \in U (w^{-1} = w \land w \circ w \subseteq V)$