Metamath Proof Explorer

Theorem ustrel

Description: The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017)

Ref Expression
Assertion ustrel 
|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> Rel V )

Proof

Step Hyp Ref Expression
1 ustssxp 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> V C_ ( X X. X ) )
2 xpss 
 |-  ( X X. X ) C_ ( _V X. _V )
3 1 2 sstrdi 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> V C_ ( _V X. _V ) )
4 df-rel 
 |-  ( Rel V <-> V C_ ( _V X. _V ) )
5 3 4 sylibr 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> Rel V )