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