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	$$⊢\left(V\subseteq X\times X\wedge A\in X\right)\to V\left[\left\{A\right\}\right]\times V\left[\left\{A\right\}\right]\subseteq V\circ V^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		snnzg	$$⊢A\in X\to \left\{A\right\}\ne \varnothing$$
2	1	adantl	$$⊢\left(V\subseteq X\times X\wedge A\in X\right)\to \left\{A\right\}\ne \varnothing$$
3		xpco	$$⊢\left\{A\right\}\ne \varnothing \to \left(\left\{A\right\}\times V\left[\left\{A\right\}\right]\right)\circ \left(V\left[\left\{A\right\}\right]\times \left\{A\right\}\right)=V\left[\left\{A\right\}\right]\times V\left[\left\{A\right\}\right]$$
4	2 3	syl	$$⊢\left(V\subseteq X\times X\wedge A\in X\right)\to \left(\left\{A\right\}\times V\left[\left\{A\right\}\right]\right)\circ \left(V\left[\left\{A\right\}\right]\times \left\{A\right\}\right)=V\left[\left\{A\right\}\right]\times V\left[\left\{A\right\}\right]$$
5		cnvxp	$$⊢{\left(\left\{A\right\}\times V\left[\left\{A\right\}\right]\right)}^{-1}=V\left[\left\{A\right\}\right]\times \left\{A\right\}$$
6		ressn	$$⊢{V\upharpoonright }_{\left\{A\right\}}=\left\{A\right\}\times V\left[\left\{A\right\}\right]$$
7	6	cnveqi	$$⊢{\left({V\upharpoonright }_{\left\{A\right\}}\right)}^{-1}={\left(\left\{A\right\}\times V\left[\left\{A\right\}\right]\right)}^{-1}$$
8		resss	$$⊢{V\upharpoonright }_{\left\{A\right\}}\subseteq V$$
9		cnvss	$$⊢{V\upharpoonright }_{\left\{A\right\}}\subseteq V\to {\left({V\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\subseteq V^{-1}$$
10	8 9	ax-mp	$$⊢{\left({V\upharpoonright }_{\left\{A\right\}}\right)}^{-1}\subseteq V^{-1}$$
11	7 10	eqsstrri	$$⊢{\left(\left\{A\right\}\times V\left[\left\{A\right\}\right]\right)}^{-1}\subseteq V^{-1}$$
12	5 11	eqsstrri	$$⊢V\left[\left\{A\right\}\right]\times \left\{A\right\}\subseteq V^{-1}$$
13		coss2	$$⊢V\left[\left\{A\right\}\right]\times \left\{A\right\}\subseteq V^{-1}\to \left(\left\{A\right\}\times V\left[\left\{A\right\}\right]\right)\circ \left(V\left[\left\{A\right\}\right]\times \left\{A\right\}\right)\subseteq \left(\left\{A\right\}\times V\left[\left\{A\right\}\right]\right)\circ V^{-1}$$
14	12 13	mp1i	$$⊢\left(V\subseteq X\times X\wedge A\in X\right)\to \left(\left\{A\right\}\times V\left[\left\{A\right\}\right]\right)\circ \left(V\left[\left\{A\right\}\right]\times \left\{A\right\}\right)\subseteq \left(\left\{A\right\}\times V\left[\left\{A\right\}\right]\right)\circ V^{-1}$$
15	6 8	eqsstrri	$$⊢\left\{A\right\}\times V\left[\left\{A\right\}\right]\subseteq V$$
16		coss1	$$⊢\left\{A\right\}\times V\left[\left\{A\right\}\right]\subseteq V\to \left(\left\{A\right\}\times V\left[\left\{A\right\}\right]\right)\circ V^{-1}\subseteq V\circ V^{-1}$$
17	15 16	mp1i	$$⊢\left(V\subseteq X\times X\wedge A\in X\right)\to \left(\left\{A\right\}\times V\left[\left\{A\right\}\right]\right)\circ V^{-1}\subseteq V\circ V^{-1}$$
18	14 17	sstrd	$$⊢\left(V\subseteq X\times X\wedge A\in X\right)\to \left(\left\{A\right\}\times V\left[\left\{A\right\}\right]\right)\circ \left(V\left[\left\{A\right\}\right]\times \left\{A\right\}\right)\subseteq V\circ V^{-1}$$
19	4 18	eqsstrrd	$$⊢\left(V\subseteq X\times X\wedge A\in X\right)\to V\left[\left\{A\right\}\right]\times V\left[\left\{A\right\}\right]\subseteq V\circ V^{-1}$$