Metamath Proof Explorer

Theorem 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 ${⊢}\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 \left({w}\circ {w}\right)\subseteq {V}\right)$

Proof

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