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 ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to {V}\subseteq {V}\circ {V}$

Proof

Step Hyp Ref Expression
1 ssun1 ${⊢}{V}\subseteq {V}\cup \left({V}\circ {V}\right)$
2 coires1 ${⊢}{V}\circ \left({\mathrm{I}↾}_{{X}}\right)={{V}↾}_{{X}}$
3 ustrel ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \mathrm{Rel}{V}$
4 ustssxp ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to {V}\subseteq {X}×{X}$
5 dmss ${⊢}{V}\subseteq {X}×{X}\to \mathrm{dom}{V}\subseteq \mathrm{dom}\left({X}×{X}\right)$
6 4 5 syl ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \mathrm{dom}{V}\subseteq \mathrm{dom}\left({X}×{X}\right)$
7 dmxpid ${⊢}\mathrm{dom}\left({X}×{X}\right)={X}$
8 6 7 sseqtrdi ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \mathrm{dom}{V}\subseteq {X}$
9 relssres ${⊢}\left(\mathrm{Rel}{V}\wedge \mathrm{dom}{V}\subseteq {X}\right)\to {{V}↾}_{{X}}={V}$
10 3 8 9 syl2anc ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to {{V}↾}_{{X}}={V}$
11 2 10 syl5eq ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to {V}\circ \left({\mathrm{I}↾}_{{X}}\right)={V}$
12 11 uneq1d ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \left({V}\circ \left({\mathrm{I}↾}_{{X}}\right)\right)\cup \left({V}\circ {V}\right)={V}\cup \left({V}\circ {V}\right)$
13 1 12 sseqtrrid ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to {V}\subseteq \left({V}\circ \left({\mathrm{I}↾}_{{X}}\right)\right)\cup \left({V}\circ {V}\right)$
14 coundi ${⊢}{V}\circ \left(\left({\mathrm{I}↾}_{{X}}\right)\cup {V}\right)=\left({V}\circ \left({\mathrm{I}↾}_{{X}}\right)\right)\cup \left({V}\circ {V}\right)$
15 13 14 sseqtrrdi ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to {V}\subseteq {V}\circ \left(\left({\mathrm{I}↾}_{{X}}\right)\cup {V}\right)$
16 ustdiag ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to {\mathrm{I}↾}_{{X}}\subseteq {V}$
17 ssequn1 ${⊢}{\mathrm{I}↾}_{{X}}\subseteq {V}↔\left({\mathrm{I}↾}_{{X}}\right)\cup {V}={V}$
18 16 17 sylib ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to \left({\mathrm{I}↾}_{{X}}\right)\cup {V}={V}$
19 18 coeq2d ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to {V}\circ \left(\left({\mathrm{I}↾}_{{X}}\right)\cup {V}\right)={V}\circ {V}$
20 15 19 sseqtrd ${⊢}\left({U}\in \mathrm{UnifOn}\left({X}\right)\wedge {V}\in {U}\right)\to {V}\subseteq {V}\circ {V}$