Metamath Proof Explorer

Theorem resttop

Description: A subspace topology is a topology. Definition of subspace topology in Munkres p. 89. A is normally a subset of the base set of J . (Contributed by FL, 15-Apr-2007) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion resttop ⊢ J ∈ Top ∧ A ∈ V → J ↾ 𝑡 A ∈ Top

Proof

Step Hyp Ref Expression
1 tgrest ⊢ J ∈ Top ∧ A ∈ V → topGen ⁡ J ↾ 𝑡 A = topGen ⁡ J ↾ 𝑡 A
2 tgtop ⊢ J ∈ Top → topGen ⁡ J = J
3 2 adantr ⊢ J ∈ Top ∧ A ∈ V → topGen ⁡ J = J
4 3 oveq1d ⊢ J ∈ Top ∧ A ∈ V → topGen ⁡ J ↾ 𝑡 A = J ↾ 𝑡 A
5 1 4 eqtrd ⊢ J ∈ Top ∧ A ∈ V → topGen ⁡ J ↾ 𝑡 A = J ↾ 𝑡 A
6 topbas ⊢ J ∈ Top → J ∈ TopBases
7 6 adantr ⊢ J ∈ Top ∧ A ∈ V → J ∈ TopBases
8 restbas ⊢ J ∈ TopBases → J ↾ 𝑡 A ∈ TopBases
9 tgcl ⊢ J ↾ 𝑡 A ∈ TopBases → topGen ⁡ J ↾ 𝑡 A ∈ Top
10 7 8 9 3syl ⊢ J ∈ Top ∧ A ∈ V → topGen ⁡ J ↾ 𝑡 A ∈ Top
11 5 10 eqeltrrd ⊢ J ∈ Top ∧ A ∈ V → J ↾ 𝑡 A ∈ Top