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 X × X A X V A × V A V V -1

Proof

Step Hyp Ref Expression
1 snnzg A X A
2 1 adantl V X × X A X A
3 xpco A A × V A V A × A = V A × V A
4 2 3 syl V X × X A X A × V A V A × A = V A × V A
5 cnvxp A × V A -1 = V A × A
6 ressn V A = A × V A
7 6 cnveqi V A -1 = A × V A -1
8 resss V A V
9 cnvss V A V V A -1 V -1
10 8 9 ax-mp V A -1 V -1
11 7 10 eqsstrri A × V A -1 V -1
12 5 11 eqsstrri V A × A V -1
13 coss2 V A × A V -1 A × V A V A × A A × V A V -1
14 12 13 mp1i V X × X A X A × V A V A × A A × V A V -1
15 6 8 eqsstrri A × V A V
16 coss1 A × V A V A × V A V -1 V V -1
17 15 16 mp1i V X × X A X A × V A V -1 V V -1
18 14 17 sstrd V X × X A X A × V A V A × A V V -1
19 4 18 eqsstrrd V X × X A X V A × V A V V -1