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