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

Metamath Proof Explorer

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 )