ressust

Description: The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22-Jan-2018)

	Ref	Expression
Hypotheses	ressust.x	$⊢ X = {Base}_{W}$
	ressust.t	$⊢ T = UnifSt (W ↾_{𝑠} A)$
Assertion	ressust	$⊢ (W \in UnifSp \land A \subseteq X) \to T \in UnifOn (A)$

Step	Hyp	Ref	Expression
1		ressust.x	$⊢ X = {Base}_{W}$
2		ressust.t	$⊢ T = UnifSt (W ↾_{𝑠} A)$
3	1	fvexi	$⊢ X \in V$
4	3	ssex	$⊢ A \subseteq X \to A \in V$
5	4	adantl	$⊢ (W \in UnifSp \land A \subseteq X) \to A \in V$
6		ressuss	$⊢ A \in V \to UnifSt (W ↾_{𝑠} A) = UnifSt (W) ↾_{𝑡} (A \times A)$
7	5 6	syl	$⊢ (W \in UnifSp \land A \subseteq X) \to UnifSt (W ↾_{𝑠} A) = UnifSt (W) ↾_{𝑡} (A \times A)$
8	2 7	eqtrid	$⊢ (W \in UnifSp \land A \subseteq X) \to T = UnifSt (W) ↾_{𝑡} (A \times A)$
9		eqid	$⊢ UnifSt (W) = UnifSt (W)$
10		eqid	$⊢ TopOpen (W) = TopOpen (W)$
11	1 9 10	isusp	$⊢ W \in UnifSp \leftrightarrow (UnifSt (W) \in UnifOn (X) \land TopOpen (W) = unifTop (UnifSt (W)))$
12	11	simplbi	$⊢ W \in UnifSp \to UnifSt (W) \in UnifOn (X)$
13		trust	$⊢ (UnifSt (W) \in UnifOn (X) \land A \subseteq X) \to UnifSt (W) ↾_{𝑡} (A \times A) \in UnifOn (A)$
14	12 13	sylan	$⊢ (W \in UnifSp \land A \subseteq X) \to UnifSt (W) ↾_{𝑡} (A \times A) \in UnifOn (A)$
15	8 14	eqeltrd	$⊢ (W \in UnifSp \land A \subseteq X) \to T \in UnifOn (A)$

Metamath Proof Explorer