resstps

Description: A restricted topological space is a topological space. Note that this theorem would not be true if TopSp was defined directly in terms of the TopSet slot instead of the TopOpen derived function. (Contributed by Mario Carneiro, 13-Aug-2015)

		Ref	Expression
	Assertion	resstps	$⊢ (K \in TopSp \land A \in V) \to K ↾_{𝑠} A \in TopSp$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{K} = {Base}_{K}$
2		eqid	$⊢ TopOpen (K) = TopOpen (K)$
3	1 2	istps	$⊢ K \in TopSp \leftrightarrow TopOpen (K) \in TopOn ({Base}_{K})$
4		resttopon2	$⊢ (TopOpen (K) \in TopOn ({Base}_{K}) \land A \in V) \to TopOpen (K) ↾_{𝑡} A \in TopOn (A \cap {Base}_{K})$
5	3 4	sylanb	$⊢ (K \in TopSp \land A \in V) \to TopOpen (K) ↾_{𝑡} A \in TopOn (A \cap {Base}_{K})$
6		eqid	$⊢ K ↾_{𝑠} A = K ↾_{𝑠} A$
7	6 1	ressbas	$⊢ A \in V \to A \cap {Base}_{K} = {Base}_{(K ↾_{𝑠} A)}$
8	7	adantl	$⊢ (K \in TopSp \land A \in V) \to A \cap {Base}_{K} = {Base}_{(K ↾_{𝑠} A)}$
9	8	fveq2d	$⊢ (K \in TopSp \land A \in V) \to TopOn (A \cap {Base}_{K}) = TopOn ({Base}_{(K ↾_{𝑠} A)})$
10	5 9	eleqtrd	$⊢ (K \in TopSp \land A \in V) \to TopOpen (K) ↾_{𝑡} A \in TopOn ({Base}_{(K ↾_{𝑠} A)})$
11		eqid	$⊢ {Base}_{(K ↾_{𝑠} A)} = {Base}_{(K ↾_{𝑠} A)}$
12	6 2	resstopn	$⊢ TopOpen (K) ↾_{𝑡} A = TopOpen (K ↾_{𝑠} A)$
13	11 12	istps	$⊢ K ↾_{𝑠} A \in TopSp \leftrightarrow TopOpen (K) ↾_{𝑡} A \in TopOn ({Base}_{(K ↾_{𝑠} A)})$
14	10 13	sylibr	$⊢ (K \in TopSp \land A \in V) \to K ↾_{𝑠} A \in TopSp$

Metamath Proof Explorer

Theorem resstps

Proof