ustssxp

Description: Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017)

		Ref	Expression
	Assertion	ustssxp	$⊢ (U \in UnifOn (X) \land V \in U) \to V \subseteq X \times X$

Step	Hyp	Ref	Expression
1		elfvex	$⊢ U \in UnifOn (X) \to X \in V$
2		isust	$⊢ X \in V \to (U \in UnifOn (X) \leftrightarrow (U \subseteq 𝒫 (X \times X) \land X \times X \in U \land \forall v \in U (\forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U) \land \forall w \in U v \cap w \in U \land ({I ↾}_{X} \subseteq v \land v^{-1} \in U \land \exists w \in U w \circ w \subseteq v))))$
3	1 2	syl	$⊢ U \in UnifOn (X) \to (U \in UnifOn (X) \leftrightarrow (U \subseteq 𝒫 (X \times X) \land X \times X \in U \land \forall v \in U (\forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U) \land \forall w \in U v \cap w \in U \land ({I ↾}_{X} \subseteq v \land v^{-1} \in U \land \exists w \in U w \circ w \subseteq v))))$
4	3	ibi	$⊢ U \in UnifOn (X) \to (U \subseteq 𝒫 (X \times X) \land X \times X \in U \land \forall v \in U (\forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U) \land \forall w \in U v \cap w \in U \land ({I ↾}_{X} \subseteq v \land v^{-1} \in U \land \exists w \in U w \circ w \subseteq v)))$
5	4	simp1d	$⊢ U \in UnifOn (X) \to U \subseteq 𝒫 (X \times X)$
6	5	sselda	$⊢ (U \in UnifOn (X) \land V \in U) \to V \in 𝒫 (X \times X)$
7	6	elpwid	$⊢ (U \in UnifOn (X) \land V \in U) \to V \subseteq X \times X$

Metamath Proof Explorer