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

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