This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ UnifOn ⁡ X ∧ V ∈ U → ∃ w ∈ U w -1 = w ∧ w ∘ w ⊆ V

Proof

Step Hyp Ref Expression
1 ustexsym ⊢ U ∈ UnifOn ⁡ X ∧ v ∈ U → ∃ w ∈ U w -1 = w ∧ w ⊆ v
2 1 ad4ant13 ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ v ∈ U ∧ v ∘ v ⊆ V → ∃ w ∈ U w -1 = w ∧ w ⊆ v
3 simprl ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ v ∈ U ∧ v ∘ v ⊆ V ∧ w ∈ U ∧ w -1 = w ∧ w ⊆ v → w -1 = w
4 coss1 ⊢ w ⊆ v → w ∘ w ⊆ v ∘ w
5 coss2 ⊢ w ⊆ v → v ∘ w ⊆ v ∘ v
6 4 5 sstrd ⊢ w ⊆ v → w ∘ w ⊆ v ∘ v
7 6 ad2antll ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ v ∈ U ∧ v ∘ v ⊆ V ∧ w ∈ U ∧ w -1 = w ∧ w ⊆ v → w ∘ w ⊆ v ∘ v
8 simpllr ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ v ∈ U ∧ v ∘ v ⊆ V ∧ w ∈ U ∧ w -1 = w ∧ w ⊆ v → v ∘ v ⊆ V
9 7 8 sstrd ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ v ∈ U ∧ v ∘ v ⊆ V ∧ w ∈ U ∧ w -1 = w ∧ w ⊆ v → w ∘ w ⊆ V
10 3 9 jca ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ v ∈ U ∧ v ∘ v ⊆ V ∧ w ∈ U ∧ w -1 = w ∧ w ⊆ v → w -1 = w ∧ w ∘ w ⊆ V
11 10 ex ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ v ∈ U ∧ v ∘ v ⊆ V ∧ w ∈ U → w -1 = w ∧ w ⊆ v → w -1 = w ∧ w ∘ w ⊆ V
12 11 reximdva ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ v ∈ U ∧ v ∘ v ⊆ V → ∃ w ∈ U w -1 = w ∧ w ⊆ v → ∃ w ∈ U w -1 = w ∧ w ∘ w ⊆ V
13 2 12 mpd ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U ∧ v ∈ U ∧ v ∘ v ⊆ V → ∃ w ∈ U w -1 = w ∧ w ∘ w ⊆ V
14 ustexhalf ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → ∃ v ∈ U v ∘ v ⊆ V
15 13 14 r19.29a ⊢ U ∈ UnifOn ⁡ X ∧ V ∈ U → ∃ w ∈ U w -1 = w ∧ w ∘ w ⊆ V