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