Theorem 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	⊢ ( ( 𝐾 ∈ TopSp ∧ 𝐴 ∈ 𝑉 ) → ( 𝐾 ↾s 𝐴 ) ∈ TopSp )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
2		eqid	⊢ ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 )
3	1 2	istps	⊢ ( 𝐾 ∈ TopSp ↔ ( TopOpen ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) )
4		resttopon2	⊢ ( ( ( TopOpen ‘ 𝐾 ) ∈ ( TopOn ‘ ( Base ‘ 𝐾 ) ) ∧ 𝐴 ∈ 𝑉 ) → ( ( TopOpen ‘ 𝐾 ) ↾t 𝐴 ) ∈ ( TopOn ‘ ( 𝐴 ∩ ( Base ‘ 𝐾 ) ) ) )
5	3 4	sylanb	⊢ ( ( 𝐾 ∈ TopSp ∧ 𝐴 ∈ 𝑉 ) → ( ( TopOpen ‘ 𝐾 ) ↾t 𝐴 ) ∈ ( TopOn ‘ ( 𝐴 ∩ ( Base ‘ 𝐾 ) ) ) )
6		eqid	⊢ ( 𝐾 ↾s 𝐴 ) = ( 𝐾 ↾s 𝐴 )
7	6 1	ressbas	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ ( Base ‘ 𝐾 ) ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
8	7	adantl	⊢ ( ( 𝐾 ∈ TopSp ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 ∩ ( Base ‘ 𝐾 ) ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
9	8	fveq2d	⊢ ( ( 𝐾 ∈ TopSp ∧ 𝐴 ∈ 𝑉 ) → ( TopOn ‘ ( 𝐴 ∩ ( Base ‘ 𝐾 ) ) ) = ( TopOn ‘ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) )
10	5 9	eleqtrd	⊢ ( ( 𝐾 ∈ TopSp ∧ 𝐴 ∈ 𝑉 ) → ( ( TopOpen ‘ 𝐾 ) ↾t 𝐴 ) ∈ ( TopOn ‘ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) )
11		eqid	⊢ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) )
12	6 2	resstopn	⊢ ( ( TopOpen ‘ 𝐾 ) ↾t 𝐴 ) = ( TopOpen ‘ ( 𝐾 ↾s 𝐴 ) )
13	11 12	istps	⊢ ( ( 𝐾 ↾s 𝐴 ) ∈ TopSp ↔ ( ( TopOpen ‘ 𝐾 ) ↾t 𝐴 ) ∈ ( TopOn ‘ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ) )
14	10 13	sylibr	⊢ ( ( 𝐾 ∈ TopSp ∧ 𝐴 ∈ 𝑉 ) → ( 𝐾 ↾s 𝐴 ) ∈ TopSp )