This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) )