Metamath Proof Explorer

Theorem ustneism

Description: For a point A in X , ( V " { A } ) is small enough in ( V o.`' V ) ` . This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 18-Nov-2017)

Ref Expression
Assertion ustneism 
|- ( ( V C_ ( X X. X ) /\ A e. X ) -> ( ( V " { A } ) X. ( V " { A } ) ) C_ ( V o. `' V ) )

Proof

Step Hyp Ref Expression
1 snnzg 
 |-  ( A e. X -> { A } =/= (/) )
2 1 adantl 
 |-  ( ( V C_ ( X X. X ) /\ A e. X ) -> { A } =/= (/) )
3 xpco 
 |-  ( { A } =/= (/) -> ( ( { A } X. ( V " { A } ) ) o. ( ( V " { A } ) X. { A } ) ) = ( ( V " { A } ) X. ( V " { A } ) ) )
4 2 3 syl 
 |-  ( ( V C_ ( X X. X ) /\ A e. X ) -> ( ( { A } X. ( V " { A } ) ) o. ( ( V " { A } ) X. { A } ) ) = ( ( V " { A } ) X. ( V " { A } ) ) )
5 cnvxp 
 |-  `' ( { A } X. ( V " { A } ) ) = ( ( V " { A } ) X. { A } )
6 ressn 
 |-  ( V |` { A } ) = ( { A } X. ( V " { A } ) )
7 6 cnveqi 
 |-  `' ( V |` { A } ) = `' ( { A } X. ( V " { A } ) )
8 resss 
 |-  ( V |` { A } ) C_ V
9 cnvss 
 |-  ( ( V |` { A } ) C_ V -> `' ( V |` { A } ) C_ `' V )
10 8 9 ax-mp 
 |-  `' ( V |` { A } ) C_ `' V
11 7 10 eqsstrri 
 |-  `' ( { A } X. ( V " { A } ) ) C_ `' V
12 5 11 eqsstrri 
 |-  ( ( V " { A } ) X. { A } ) C_ `' V
13 coss2 
 |-  ( ( ( V " { A } ) X. { A } ) C_ `' V -> ( ( { A } X. ( V " { A } ) ) o. ( ( V " { A } ) X. { A } ) ) C_ ( ( { A } X. ( V " { A } ) ) o. `' V ) )
14 12 13 mp1i 
 |-  ( ( V C_ ( X X. X ) /\ A e. X ) -> ( ( { A } X. ( V " { A } ) ) o. ( ( V " { A } ) X. { A } ) ) C_ ( ( { A } X. ( V " { A } ) ) o. `' V ) )
15 6 8 eqsstrri 
 |-  ( { A } X. ( V " { A } ) ) C_ V
16 coss1 
 |-  ( ( { A } X. ( V " { A } ) ) C_ V -> ( ( { A } X. ( V " { A } ) ) o. `' V ) C_ ( V o. `' V ) )
17 15 16 mp1i 
 |-  ( ( V C_ ( X X. X ) /\ A e. X ) -> ( ( { A } X. ( V " { A } ) ) o. `' V ) C_ ( V o. `' V ) )
18 14 17 sstrd 
 |-  ( ( V C_ ( X X. X ) /\ A e. X ) -> ( ( { A } X. ( V " { A } ) ) o. ( ( V " { A } ) X. { A } ) ) C_ ( V o. `' V ) )
19 4 18 eqsstrrd 
 |-  ( ( V C_ ( X X. X ) /\ A e. X ) -> ( ( V " { A } ) X. ( V " { A } ) ) C_ ( V o. `' V ) )