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 e. ( UnifOn ` X ) /\ V e. U ) -> V C_ ( V o. V ) )

Proof

Step	Hyp	Ref	Expression
1		ssun1	|- V C_ ( V u. ( V o. V ) )
2		coires1	|- ( V o. ( _I |` X ) ) = ( V |` X )
3		ustrel	|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> Rel V )
4		ustssxp	|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> V C_ ( X X. X ) )
5		dmss	|- ( V C_ ( X X. X ) -> dom V C_ dom ( X X. X ) )
6	4 5	syl	|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> dom V C_ dom ( X X. X ) )
7		dmxpid	|- dom ( X X. X ) = X
8	6 7	sseqtrdi	|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> dom V C_ X )
9		relssres	|- ( ( Rel V /\ dom V C_ X ) -> ( V |` X ) = V )
10	3 8 9	syl2anc	|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> ( V |` X ) = V )
11	2 10	eqtrid	|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> ( V o. ( _I |` X ) ) = V )
12	11	uneq1d	|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> ( ( V o. ( _I |` X ) ) u. ( V o. V ) ) = ( V u. ( V o. V ) ) )
13	1 12	sseqtrrid	|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> V C_ ( ( V o. ( _I |` X ) ) u. ( V o. V ) ) )
14		coundi	|- ( V o. ( ( _I |` X ) u. V ) ) = ( ( V o. ( _I |` X ) ) u. ( V o. V ) )
15	13 14	sseqtrrdi	|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> V C_ ( V o. ( ( _I |` X ) u. V ) ) )
16		ustdiag	|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> ( _I |` X ) C_ V )
17		ssequn1	|- ( ( _I |` X ) C_ V <-> ( ( _I |` X ) u. V ) = V )
18	16 17	sylib	|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> ( ( _I |` X ) u. V ) = V )
19	18	coeq2d	|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> ( V o. ( ( _I |` X ) u. V ) ) = ( V o. V ) )
20	15 19	sseqtrd	|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> V C_ ( V o. V ) )