ustex3sym

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

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

Proof

Step	Hyp	Ref	Expression
1		ustex2sym	$⊢ (U \in UnifOn (X) \land v \in U) \to \exists w \in U (w^{-1} = w \land w \circ 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 \circ 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 \circ w \subseteq v)) \to w^{-1} = w$
4		simp-5l	$⊢ (((((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 \circ w \subseteq v)) \to U \in UnifOn (X)$
5		simplr	$⊢ (((((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 \circ w \subseteq v)) \to w \in U$
6		ustssco	$⊢ (U \in UnifOn (X) \land w \in U) \to w \subseteq w \circ w$
7	4 5 6	syl2anc	$⊢ (((((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 \circ w \subseteq v)) \to w \subseteq w \circ w$
8		simprr	$⊢ (((((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 \circ w \subseteq v)) \to w \circ w \subseteq v$
9		coss2	$⊢ w \circ w \subseteq v \to w \circ (w \circ w) \subseteq w \circ v$
10	9	adantl	$⊢ (w \subseteq w \circ w \land w \circ w \subseteq v) \to w \circ (w \circ w) \subseteq w \circ v$
11		sstr	$⊢ (w \subseteq w \circ w \land w \circ w \subseteq v) \to w \subseteq v$
12		coss1	$⊢ w \subseteq v \to w \circ v \subseteq v \circ v$
13	11 12	syl	$⊢ (w \subseteq w \circ w \land w \circ w \subseteq v) \to w \circ v \subseteq v \circ v$
14	10 13	sstrd	$⊢ (w \subseteq w \circ w \land w \circ w \subseteq v) \to w \circ (w \circ w) \subseteq v \circ v$
15	7 8 14	syl2anc	$⊢ (((((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 \circ w \subseteq v)) \to w \circ (w \circ w) \subseteq v \circ v$
16		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 \circ w \subseteq v)) \to v \circ v \subseteq V$
17	15 16	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 \circ w \subseteq v)) \to w \circ (w \circ w) \subseteq V$
18	3 17	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 \circ w \subseteq v)) \to (w^{-1} = w \land w \circ (w \circ w) \subseteq V)$
19	18	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 \circ w \subseteq v) \to (w^{-1} = w \land w \circ (w \circ w) \subseteq V))$
20	19	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 \circ w \subseteq v) \to \exists w \in U (w^{-1} = w \land w \circ (w \circ w) \subseteq V))$
21	2 20	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 \circ w) \subseteq V)$
22		ustexhalf	$⊢ (U \in UnifOn (X) \land V \in U) \to \exists v \in U v \circ v \subseteq V$
23	21 22	r19.29a	$⊢ (U \in UnifOn (X) \land V \in U) \to \exists w \in U (w^{-1} = w \land w \circ (w \circ w) \subseteq V)$

Metamath Proof Explorer

Theorem ustex3sym

Proof