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

Metamath Proof Explorer

Theorem ustexsym

Description: In an uniform structure, for any entourage V , there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018)

Ref Expression
Assertion ustexsym ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → ∃ 𝑤 ∈ 𝑈 ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 simplll ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑉 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
2 ustinvel ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑈 ) → ◡ 𝑥 ∈ 𝑈 )
3 2 ad4ant13 ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑉 ) → ◡ 𝑥 ∈ 𝑈 )
4 simplr ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑉 ) → 𝑥 ∈ 𝑈 )
5 ustincl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ◡ 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈 ) → ( ◡ 𝑥 ∩ 𝑥 ) ∈ 𝑈 )
6 1 3 4 5 syl3anc ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑉 ) → ( ◡ 𝑥 ∩ 𝑥 ) ∈ 𝑈 )
7 ustrel ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑈 ) → Rel 𝑥 )
8 dfrel2 ⊢ ( Rel 𝑥 ↔ ◡ ◡ 𝑥 = 𝑥 )
9 7 8 sylib ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑈 ) → ◡ ◡ 𝑥 = 𝑥 )
10 9 ineq1d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑈 ) → ( ◡ ◡ 𝑥 ∩ ◡ 𝑥 ) = ( 𝑥 ∩ ◡ 𝑥 ) )
11 cnvin ⊢ ◡ ( ◡ 𝑥 ∩ 𝑥 ) = ( ◡ ◡ 𝑥 ∩ ◡ 𝑥 )
12 incom ⊢ ( ◡ 𝑥 ∩ 𝑥 ) = ( 𝑥 ∩ ◡ 𝑥 )
13 10 11 12 3eqtr4g ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑈 ) → ◡ ( ◡ 𝑥 ∩ 𝑥 ) = ( ◡ 𝑥 ∩ 𝑥 ) )
14 13 ad4ant13 ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑉 ) → ◡ ( ◡ 𝑥 ∩ 𝑥 ) = ( ◡ 𝑥 ∩ 𝑥 ) )
15 inss2 ⊢ ( ◡ 𝑥 ∩ 𝑥 ) ⊆ 𝑥
16 ustssco ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ⊆ ( 𝑥 ∘ 𝑥 ) )
17 16 ad4ant13 ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑉 ) → 𝑥 ⊆ ( 𝑥 ∘ 𝑥 ) )
18 simpr ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑉 ) → ( 𝑥 ∘ 𝑥 ) ⊆ 𝑉 )
19 17 18 sstrd ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑉 ) → 𝑥 ⊆ 𝑉 )
20 15 19 sstrid ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑉 ) → ( ◡ 𝑥 ∩ 𝑥 ) ⊆ 𝑉 )
21 cnveq ⊢ ( 𝑤 = ( ◡ 𝑥 ∩ 𝑥 ) → ◡ 𝑤 = ◡ ( ◡ 𝑥 ∩ 𝑥 ) )
22 id ⊢ ( 𝑤 = ( ◡ 𝑥 ∩ 𝑥 ) → 𝑤 = ( ◡ 𝑥 ∩ 𝑥 ) )
23 21 22 eqeq12d ⊢ ( 𝑤 = ( ◡ 𝑥 ∩ 𝑥 ) → ( ◡ 𝑤 = 𝑤 ↔ ◡ ( ◡ 𝑥 ∩ 𝑥 ) = ( ◡ 𝑥 ∩ 𝑥 ) ) )
24 sseq1 ⊢ ( 𝑤 = ( ◡ 𝑥 ∩ 𝑥 ) → ( 𝑤 ⊆ 𝑉 ↔ ( ◡ 𝑥 ∩ 𝑥 ) ⊆ 𝑉 ) )
25 23 24 anbi12d ⊢ ( 𝑤 = ( ◡ 𝑥 ∩ 𝑥 ) → ( ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑉 ) ↔ ( ◡ ( ◡ 𝑥 ∩ 𝑥 ) = ( ◡ 𝑥 ∩ 𝑥 ) ∧ ( ◡ 𝑥 ∩ 𝑥 ) ⊆ 𝑉 ) ) )
26 25 rspcev ⊢ ( ( ( ◡ 𝑥 ∩ 𝑥 ) ∈ 𝑈 ∧ ( ◡ ( ◡ 𝑥 ∩ 𝑥 ) = ( ◡ 𝑥 ∩ 𝑥 ) ∧ ( ◡ 𝑥 ∩ 𝑥 ) ⊆ 𝑉 ) ) → ∃ 𝑤 ∈ 𝑈 ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑉 ) )
27 6 14 20 26 syl12anc ⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑉 ) → ∃ 𝑤 ∈ 𝑈 ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑉 ) )
28 ustexhalf ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → ∃ 𝑥 ∈ 𝑈 ( 𝑥 ∘ 𝑥 ) ⊆ 𝑉 )
29 27 28 r19.29a ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → ∃ 𝑤 ∈ 𝑈 ( ◡ 𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑉 ) )