Metamath Proof Explorer

Theorem ustref

Description: Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017)

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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  A = A
2 resieq 
 |-  ( ( A e. X /\ A e. X ) -> ( A ( _I |` X ) A <-> A = A ) )
3 1 2 mpbiri 
 |-  ( ( A e. X /\ A e. X ) -> A ( _I |` X ) A )
4 3 anidms 
 |-  ( A e. X -> A ( _I |` X ) A )
5 4 3ad2ant3 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ A e. X ) -> A ( _I |` X ) A )
6 ustdiag 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> ( _I |` X ) C_ V )
7 6 ssbrd 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> ( A ( _I |` X ) A -> A V A ) )
8 7 3adant3 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ A e. X ) -> ( A ( _I |` X ) A -> A V A ) )
9 5 8 mpd 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ A e. X ) -> A V A )