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

Proof

Step Hyp Ref Expression
1 ustexsym ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑣 ∈ 𝑈 ) → ∃ 𝑤 ∈ 𝑈 ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑣 ) )
2 1 ad4ant13 ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑣 ∘ 𝑣 ) ⊆ 𝑉 ) → ∃ 𝑤 ∈ 𝑈 ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑣 ) )
3 simprl ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑣 ∘ 𝑣 ) ⊆ 𝑉 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) → ◡ 𝑤 = 𝑤 )
4 coss1 ⊢ ( 𝑤 ⊆ 𝑣 → ( 𝑤 ∘ 𝑤 ) ⊆ ( 𝑣 ∘ 𝑤 ) )
5 coss2 ⊢ ( 𝑤 ⊆ 𝑣 → ( 𝑣 ∘ 𝑤 ) ⊆ ( 𝑣 ∘ 𝑣 ) )
6 4 5 sstrd ⊢ ( 𝑤 ⊆ 𝑣 → ( 𝑤 ∘ 𝑤 ) ⊆ ( 𝑣 ∘ 𝑣 ) )
7 6 ad2antll ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑣 ∘ 𝑣 ) ⊆ 𝑉 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) → ( 𝑤 ∘ 𝑤 ) ⊆ ( 𝑣 ∘ 𝑣 ) )
8 simpllr ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑣 ∘ 𝑣 ) ⊆ 𝑉 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) → ( 𝑣 ∘ 𝑣 ) ⊆ 𝑉 )
9 7 8 sstrd ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑣 ∘ 𝑣 ) ⊆ 𝑉 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) → ( 𝑤 ∘ 𝑤 ) ⊆ 𝑉 )
10 3 9 jca ⊢ ( ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑣 ∘ 𝑣 ) ⊆ 𝑉 ) ∧ 𝑤 ∈ 𝑈 ) ∧ ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) → ( ◡ 𝑤 = 𝑤 ∧ ( 𝑤 ∘ 𝑤 ) ⊆ 𝑉 ) )
11 10 ex ⊢ ( ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑣 ∘ 𝑣 ) ⊆ 𝑉 ) ∧ 𝑤 ∈ 𝑈 ) → ( ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑣 ) → ( ◡ 𝑤 = 𝑤 ∧ ( 𝑤 ∘ 𝑤 ) ⊆ 𝑉 ) ) )
12 11 reximdva ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑣 ∘ 𝑣 ) ⊆ 𝑉 ) → ( ∃ 𝑤 ∈ 𝑈 ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑣 ) → ∃ 𝑤 ∈ 𝑈 ( ◡ 𝑤 = 𝑤 ∧ ( 𝑤 ∘ 𝑤 ) ⊆ 𝑉 ) ) )
13 2 12 mpd ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑣 ∈ 𝑈 ) ∧ ( 𝑣 ∘ 𝑣 ) ⊆ 𝑉 ) → ∃ 𝑤 ∈ 𝑈 ( ◡ 𝑤 = 𝑤 ∧ ( 𝑤 ∘ 𝑤 ) ⊆ 𝑉 ) )
14 ustexhalf ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → ∃ 𝑣 ∈ 𝑈 ( 𝑣 ∘ 𝑣 ) ⊆ 𝑉 )
15 13 14 r19.29a ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → ∃ 𝑤 ∈ 𝑈 ( ◡ 𝑤 = 𝑤 ∧ ( 𝑤 ∘ 𝑤 ) ⊆ 𝑉 ) )