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 ⊢ K ∈ TopSp ∧ A ∈ V → K ↾ 𝑠 A ∈ TopSp

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base K = Base K
2 eqid ⊢ TopOpen ⁡ K = TopOpen ⁡ K
3 1 2 istps ⊢ K ∈ TopSp ↔ TopOpen ⁡ K ∈ TopOn ⁡ Base K
4 resttopon2 ⊢ TopOpen ⁡ K ∈ TopOn ⁡ Base K ∧ A ∈ V → TopOpen ⁡ K ↾ 𝑡 A ∈ TopOn ⁡ A ∩ Base K
5 3 4 sylanb ⊢ K ∈ TopSp ∧ A ∈ V → TopOpen ⁡ K ↾ 𝑡 A ∈ TopOn ⁡ A ∩ Base K
6 eqid ⊢ K ↾ 𝑠 A = K ↾ 𝑠 A
7 6 1 ressbas ⊢ A ∈ V → A ∩ Base K = Base K ↾ 𝑠 A
8 7 adantl ⊢ K ∈ TopSp ∧ A ∈ V → A ∩ Base K = Base K ↾ 𝑠 A
9 8 fveq2d ⊢ K ∈ TopSp ∧ A ∈ V → TopOn ⁡ A ∩ Base K = TopOn ⁡ Base K ↾ 𝑠 A
10 5 9 eleqtrd ⊢ K ∈ TopSp ∧ A ∈ V → TopOpen ⁡ K ↾ 𝑡 A ∈ 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 ∈ TopSp ↔ TopOpen ⁡ K ↾ 𝑡 A ∈ TopOn ⁡ Base K ↾ 𝑠 A
14 10 13 sylibr ⊢ K ∈ TopSp ∧ A ∈ V → K ↾ 𝑠 A ∈ TopSp