# 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 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}\left({{w}}^{-1}={w}\wedge {w}\circ {w}\subseteq {V}\right)$

### Proof

Step Hyp Ref Expression
1 ustexsym ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {v}\in {U}\right)\to \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}\left({{w}}^{-1}={w}\wedge {w}\subseteq {v}\right)$
2 1 ad4ant13 ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\wedge {v}\in {U}\right)\wedge {v}\circ {v}\subseteq {V}\right)\to \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}\left({{w}}^{-1}={w}\wedge {w}\subseteq {v}\right)$
3 simprl ${⊢}\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\wedge {v}\in {U}\right)\wedge {v}\circ {v}\subseteq {V}\right)\wedge {w}\in {U}\right)\wedge \left({{w}}^{-1}={w}\wedge {w}\subseteq {v}\right)\right)\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 ${⊢}\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\wedge {v}\in {U}\right)\wedge {v}\circ {v}\subseteq {V}\right)\wedge {w}\in {U}\right)\wedge \left({{w}}^{-1}={w}\wedge {w}\subseteq {v}\right)\right)\to {w}\circ {w}\subseteq {v}\circ {v}$
8 simpllr ${⊢}\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\wedge {v}\in {U}\right)\wedge {v}\circ {v}\subseteq {V}\right)\wedge {w}\in {U}\right)\wedge \left({{w}}^{-1}={w}\wedge {w}\subseteq {v}\right)\right)\to {v}\circ {v}\subseteq {V}$
9 7 8 sstrd ${⊢}\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\wedge {v}\in {U}\right)\wedge {v}\circ {v}\subseteq {V}\right)\wedge {w}\in {U}\right)\wedge \left({{w}}^{-1}={w}\wedge {w}\subseteq {v}\right)\right)\to {w}\circ {w}\subseteq {V}$
10 3 9 jca ${⊢}\left(\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\wedge {v}\in {U}\right)\wedge {v}\circ {v}\subseteq {V}\right)\wedge {w}\in {U}\right)\wedge \left({{w}}^{-1}={w}\wedge {w}\subseteq {v}\right)\right)\to \left({{w}}^{-1}={w}\wedge {w}\circ {w}\subseteq {V}\right)$
11 10 ex ${⊢}\left(\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\wedge {v}\in {U}\right)\wedge {v}\circ {v}\subseteq {V}\right)\wedge {w}\in {U}\right)\to \left(\left({{w}}^{-1}={w}\wedge {w}\subseteq {v}\right)\to \left({{w}}^{-1}={w}\wedge {w}\circ {w}\subseteq {V}\right)\right)$
12 11 reximdva ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\wedge {v}\in {U}\right)\wedge {v}\circ {v}\subseteq {V}\right)\to \left(\exists {w}\in {U}\phantom{\rule{.4em}{0ex}}\left({{w}}^{-1}={w}\wedge {w}\subseteq {v}\right)\to \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}\left({{w}}^{-1}={w}\wedge {w}\circ {w}\subseteq {V}\right)\right)$
13 2 12 mpd ${⊢}\left(\left(\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\wedge {v}\in {U}\right)\wedge {v}\circ {v}\subseteq {V}\right)\to \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}\left({{w}}^{-1}={w}\wedge {w}\circ {w}\subseteq {V}\right)$
14 ustexhalf ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \exists {v}\in {U}\phantom{\rule{.4em}{0ex}}{v}\circ {v}\subseteq {V}$
15 13 14 r19.29a ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}\left({{w}}^{-1}={w}\wedge {w}\circ {w}\subseteq {V}\right)$