# 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 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) → ∃ 𝑤𝑈 ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑉 ) )

### Proof

Step Hyp Ref Expression
1 ustex2sym ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑣𝑈 ) → ∃ 𝑤𝑈 ( 𝑤 = 𝑤 ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) )
2 1 ad4ant13 ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) ∧ 𝑣𝑈 ) ∧ ( 𝑣𝑣 ) ⊆ 𝑉 ) → ∃ 𝑤𝑈 ( 𝑤 = 𝑤 ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) )
3 simprl ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) ∧ 𝑣𝑈 ) ∧ ( 𝑣𝑣 ) ⊆ 𝑉 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) ) → 𝑤 = 𝑤 )
4 simp-5l ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) ∧ 𝑣𝑈 ) ∧ ( 𝑣𝑣 ) ⊆ 𝑉 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
5 simplr ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) ∧ 𝑣𝑈 ) ∧ ( 𝑣𝑣 ) ⊆ 𝑉 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) ) → 𝑤𝑈 )
6 ustssco ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑤𝑈 ) → 𝑤 ⊆ ( 𝑤𝑤 ) )
7 4 5 6 syl2anc ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) ∧ 𝑣𝑈 ) ∧ ( 𝑣𝑣 ) ⊆ 𝑉 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) ) → 𝑤 ⊆ ( 𝑤𝑤 ) )
8 simprr ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) ∧ 𝑣𝑈 ) ∧ ( 𝑣𝑣 ) ⊆ 𝑉 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) ) → ( 𝑤𝑤 ) ⊆ 𝑣 )
9 coss2 ( ( 𝑤𝑤 ) ⊆ 𝑣 → ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ ( 𝑤𝑣 ) )
10 9 adantl ( ( 𝑤 ⊆ ( 𝑤𝑤 ) ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) → ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ ( 𝑤𝑣 ) )
11 sstr ( ( 𝑤 ⊆ ( 𝑤𝑤 ) ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) → 𝑤𝑣 )
12 coss1 ( 𝑤𝑣 → ( 𝑤𝑣 ) ⊆ ( 𝑣𝑣 ) )
13 11 12 syl ( ( 𝑤 ⊆ ( 𝑤𝑤 ) ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) → ( 𝑤𝑣 ) ⊆ ( 𝑣𝑣 ) )
14 10 13 sstrd ( ( 𝑤 ⊆ ( 𝑤𝑤 ) ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) → ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ ( 𝑣𝑣 ) )
15 7 8 14 syl2anc ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) ∧ 𝑣𝑈 ) ∧ ( 𝑣𝑣 ) ⊆ 𝑉 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) ) → ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ ( 𝑣𝑣 ) )
16 simpllr ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) ∧ 𝑣𝑈 ) ∧ ( 𝑣𝑣 ) ⊆ 𝑉 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) ) → ( 𝑣𝑣 ) ⊆ 𝑉 )
17 15 16 sstrd ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) ∧ 𝑣𝑈 ) ∧ ( 𝑣𝑣 ) ⊆ 𝑉 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) ) → ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑉 )
18 3 17 jca ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) ∧ 𝑣𝑈 ) ∧ ( 𝑣𝑣 ) ⊆ 𝑉 ) ∧ 𝑤𝑈 ) ∧ ( 𝑤 = 𝑤 ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) ) → ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑉 ) )
19 18 ex ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) ∧ 𝑣𝑈 ) ∧ ( 𝑣𝑣 ) ⊆ 𝑉 ) ∧ 𝑤𝑈 ) → ( ( 𝑤 = 𝑤 ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) → ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑉 ) ) )
20 19 reximdva ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) ∧ 𝑣𝑈 ) ∧ ( 𝑣𝑣 ) ⊆ 𝑉 ) → ( ∃ 𝑤𝑈 ( 𝑤 = 𝑤 ∧ ( 𝑤𝑤 ) ⊆ 𝑣 ) → ∃ 𝑤𝑈 ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑉 ) ) )
21 2 20 mpd ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) ∧ 𝑣𝑈 ) ∧ ( 𝑣𝑣 ) ⊆ 𝑉 ) → ∃ 𝑤𝑈 ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑉 ) )
22 ustexhalf ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) → ∃ 𝑣𝑈 ( 𝑣𝑣 ) ⊆ 𝑉 )
23 21 22 r19.29a ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) → ∃ 𝑤𝑈 ( 𝑤 = 𝑤 ∧ ( 𝑤 ∘ ( 𝑤𝑤 ) ) ⊆ 𝑉 ) )