Metamath Proof Explorer

Theorem ustelimasn

Description: Any point A is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017)

Ref Expression
Assertion ustelimasn 
|- ( ( U e. ( UnifOn ` X ) /\ V e. U /\ A e. X ) -> A e. ( V " { A } ) )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ A e. X ) -> A e. X )
2 ustdiag 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> ( _I |` X ) C_ V )
3 2 3adant3 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ A e. X ) -> ( _I |` X ) C_ V )
4 opelidres 
 |-  ( A e. X -> ( <. A , A >. e. ( _I |` X ) <-> A e. X ) )
5 4 ibir 
 |-  ( A e. X -> <. A , A >. e. ( _I |` X ) )
6 5 3ad2ant3 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ A e. X ) -> <. A , A >. e. ( _I |` X ) )
7 3 6 sseldd 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ A e. X ) -> <. A , A >. e. V )
8 elimasng 
 |-  ( ( A e. X /\ A e. X ) -> ( A e. ( V " { A } ) <-> <. A , A >. e. V ) )
9 8 anidms 
 |-  ( A e. X -> ( A e. ( V " { A } ) <-> <. A , A >. e. V ) )
10 9 biimpar 
 |-  ( ( A e. X /\ <. A , A >. e. V ) -> A e. ( V " { A } ) )
11 1 7 10 syl2anc 
 |-  ( ( U e. ( UnifOn ` X ) /\ V e. U /\ A e. X ) -> A e. ( V " { A } ) )