This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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