# Metamath Proof Explorer

## Theorem ustexhalf

Description: For each entourage V there is an entourage w that is "not more than half as large". Condition U_III of BourbakiTop1 p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017)

Ref Expression
Assertion ustexhalf ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {V}$

### Proof

Step Hyp Ref Expression
1 elfvex ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to {X}\in \mathrm{V}$
2 isust ${⊢}{X}\in \mathrm{V}\to \left({U}\in \mathrm{UnifOn}\left({X}\right)↔\left({U}\subseteq 𝒫\left({X}×{X}\right)\wedge {X}×{X}\in {U}\wedge \forall {v}\in {U}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\in 𝒫\left({X}×{X}\right)\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {w}\to {w}\in {U}\right)\wedge \forall {w}\in {U}\phantom{\rule{.4em}{0ex}}{v}\cap {w}\in {U}\wedge \left({\mathrm{I}↾}_{{X}}\subseteq {v}\wedge {{v}}^{-1}\in {U}\wedge \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {v}\right)\right)\right)\right)$
3 1 2 syl ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to \left({U}\in \mathrm{UnifOn}\left({X}\right)↔\left({U}\subseteq 𝒫\left({X}×{X}\right)\wedge {X}×{X}\in {U}\wedge \forall {v}\in {U}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\in 𝒫\left({X}×{X}\right)\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {w}\to {w}\in {U}\right)\wedge \forall {w}\in {U}\phantom{\rule{.4em}{0ex}}{v}\cap {w}\in {U}\wedge \left({\mathrm{I}↾}_{{X}}\subseteq {v}\wedge {{v}}^{-1}\in {U}\wedge \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {v}\right)\right)\right)\right)$
4 3 ibi ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to \left({U}\subseteq 𝒫\left({X}×{X}\right)\wedge {X}×{X}\in {U}\wedge \forall {v}\in {U}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\in 𝒫\left({X}×{X}\right)\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {w}\to {w}\in {U}\right)\wedge \forall {w}\in {U}\phantom{\rule{.4em}{0ex}}{v}\cap {w}\in {U}\wedge \left({\mathrm{I}↾}_{{X}}\subseteq {v}\wedge {{v}}^{-1}\in {U}\wedge \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {v}\right)\right)\right)$
5 4 simp3d ${⊢}{U}\in \mathrm{UnifOn}\left({X}\right)\to \forall {v}\in {U}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\in 𝒫\left({X}×{X}\right)\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {w}\to {w}\in {U}\right)\wedge \forall {w}\in {U}\phantom{\rule{.4em}{0ex}}{v}\cap {w}\in {U}\wedge \left({\mathrm{I}↾}_{{X}}\subseteq {v}\wedge {{v}}^{-1}\in {U}\wedge \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {v}\right)\right)$
6 sseq1 ${⊢}{v}={V}\to \left({v}\subseteq {w}↔{V}\subseteq {w}\right)$
7 6 imbi1d ${⊢}{v}={V}\to \left(\left({v}\subseteq {w}\to {w}\in {U}\right)↔\left({V}\subseteq {w}\to {w}\in {U}\right)\right)$
8 7 ralbidv ${⊢}{v}={V}\to \left(\forall {w}\in 𝒫\left({X}×{X}\right)\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {w}\to {w}\in {U}\right)↔\forall {w}\in 𝒫\left({X}×{X}\right)\phantom{\rule{.4em}{0ex}}\left({V}\subseteq {w}\to {w}\in {U}\right)\right)$
9 ineq1 ${⊢}{v}={V}\to {v}\cap {w}={V}\cap {w}$
10 9 eleq1d ${⊢}{v}={V}\to \left({v}\cap {w}\in {U}↔{V}\cap {w}\in {U}\right)$
11 10 ralbidv ${⊢}{v}={V}\to \left(\forall {w}\in {U}\phantom{\rule{.4em}{0ex}}{v}\cap {w}\in {U}↔\forall {w}\in {U}\phantom{\rule{.4em}{0ex}}{V}\cap {w}\in {U}\right)$
12 sseq2 ${⊢}{v}={V}\to \left({\mathrm{I}↾}_{{X}}\subseteq {v}↔{\mathrm{I}↾}_{{X}}\subseteq {V}\right)$
13 cnveq ${⊢}{v}={V}\to {{v}}^{-1}={{V}}^{-1}$
14 13 eleq1d ${⊢}{v}={V}\to \left({{v}}^{-1}\in {U}↔{{V}}^{-1}\in {U}\right)$
15 sseq2 ${⊢}{v}={V}\to \left({w}\circ {w}\subseteq {v}↔{w}\circ {w}\subseteq {V}\right)$
16 15 rexbidv ${⊢}{v}={V}\to \left(\exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {v}↔\exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {V}\right)$
17 12 14 16 3anbi123d ${⊢}{v}={V}\to \left(\left({\mathrm{I}↾}_{{X}}\subseteq {v}\wedge {{v}}^{-1}\in {U}\wedge \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {v}\right)↔\left({\mathrm{I}↾}_{{X}}\subseteq {V}\wedge {{V}}^{-1}\in {U}\wedge \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {V}\right)\right)$
18 8 11 17 3anbi123d ${⊢}{v}={V}\to \left(\left(\forall {w}\in 𝒫\left({X}×{X}\right)\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {w}\to {w}\in {U}\right)\wedge \forall {w}\in {U}\phantom{\rule{.4em}{0ex}}{v}\cap {w}\in {U}\wedge \left({\mathrm{I}↾}_{{X}}\subseteq {v}\wedge {{v}}^{-1}\in {U}\wedge \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {v}\right)\right)↔\left(\forall {w}\in 𝒫\left({X}×{X}\right)\phantom{\rule{.4em}{0ex}}\left({V}\subseteq {w}\to {w}\in {U}\right)\wedge \forall {w}\in {U}\phantom{\rule{.4em}{0ex}}{V}\cap {w}\in {U}\wedge \left({\mathrm{I}↾}_{{X}}\subseteq {V}\wedge {{V}}^{-1}\in {U}\wedge \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {V}\right)\right)\right)$
19 18 rspcv ${⊢}{V}\in {U}\to \left(\forall {v}\in {U}\phantom{\rule{.4em}{0ex}}\left(\forall {w}\in 𝒫\left({X}×{X}\right)\phantom{\rule{.4em}{0ex}}\left({v}\subseteq {w}\to {w}\in {U}\right)\wedge \forall {w}\in {U}\phantom{\rule{.4em}{0ex}}{v}\cap {w}\in {U}\wedge \left({\mathrm{I}↾}_{{X}}\subseteq {v}\wedge {{v}}^{-1}\in {U}\wedge \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {v}\right)\right)\to \left(\forall {w}\in 𝒫\left({X}×{X}\right)\phantom{\rule{.4em}{0ex}}\left({V}\subseteq {w}\to {w}\in {U}\right)\wedge \forall {w}\in {U}\phantom{\rule{.4em}{0ex}}{V}\cap {w}\in {U}\wedge \left({\mathrm{I}↾}_{{X}}\subseteq {V}\wedge {{V}}^{-1}\in {U}\wedge \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {V}\right)\right)\right)$
20 5 19 mpan9 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \left(\forall {w}\in 𝒫\left({X}×{X}\right)\phantom{\rule{.4em}{0ex}}\left({V}\subseteq {w}\to {w}\in {U}\right)\wedge \forall {w}\in {U}\phantom{\rule{.4em}{0ex}}{V}\cap {w}\in {U}\wedge \left({\mathrm{I}↾}_{{X}}\subseteq {V}\wedge {{V}}^{-1}\in {U}\wedge \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {V}\right)\right)$
21 20 simp3d ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \left({\mathrm{I}↾}_{{X}}\subseteq {V}\wedge {{V}}^{-1}\in {U}\wedge \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {V}\right)$
22 21 simp3d ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \exists {w}\in {U}\phantom{\rule{.4em}{0ex}}{w}\circ {w}\subseteq {V}$