Metamath Proof Explorer

Theorem ustssco

Description: In an uniform structure, any entourage V is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018)

Ref Expression
Assertion ustssco ⊢U∈UnifOn⁡X∧V∈U→V⊆V∘V

Proof

Step Hyp Ref Expression
1 ssun1 ⊢V⊆V∪V∘V
2 coires1 ⊢V∘I↾X=V↾X
3 ustrel ⊢U∈UnifOn⁡X∧V∈U→Rel⁡V
4 ustssxp ⊢U∈UnifOn⁡X∧V∈U→V⊆X×X
5 dmss ⊢V⊆X×X→dom⁡V⊆dom⁡X×X
6 4 5 syl ⊢U∈UnifOn⁡X∧V∈U→dom⁡V⊆dom⁡X×X
7 dmxpid ⊢dom⁡X×X=X
8 6 7 sseqtrdi ⊢U∈UnifOn⁡X∧V∈U→dom⁡V⊆X
9 relssres ⊢Rel⁡V∧dom⁡V⊆X→V↾X=V
10 3 8 9 syl2anc ⊢U∈UnifOn⁡X∧V∈U→V↾X=V
11 2 10 eqtrid ⊢U∈UnifOn⁡X∧V∈U→V∘I↾X=V
12 11 uneq1d ⊢U∈UnifOn⁡X∧V∈U→V∘I↾X∪V∘V=V∪V∘V
13 1 12 sseqtrrid ⊢U∈UnifOn⁡X∧V∈U→V⊆V∘I↾X∪V∘V
14 coundi ⊢V∘I↾X∪V=V∘I↾X∪V∘V
15 13 14 sseqtrrdi ⊢U∈UnifOn⁡X∧V∈U→V⊆V∘I↾X∪V
16 ustdiag ⊢U∈UnifOn⁡X∧V∈U→I↾X⊆V
17 ssequn1 ⊢I↾X⊆V↔I↾X∪V=V
18 16 17 sylib ⊢U∈UnifOn⁡X∧V∈U→I↾X∪V=V
19 18 coeq2d ⊢U∈UnifOn⁡X∧V∈U→V∘I↾X∪V=V∘V
20 15 19 sseqtrd ⊢U∈UnifOn⁡X∧V∈U→V⊆V∘V