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

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 ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )

Proof

Step Hyp Ref Expression
1 tgrest ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( topGen ‘ ( 𝐽 ↾t 𝐴 ) ) = ( ( topGen ‘ 𝐽 ) ↾t 𝐴 ) )
2 tgtop ⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )
3 2 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( topGen ‘ 𝐽 ) = 𝐽 )
4 3 oveq1d ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( ( topGen ‘ 𝐽 ) ↾t 𝐴 ) = ( 𝐽 ↾t 𝐴 ) )
5 1 4 eqtrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( topGen ‘ ( 𝐽 ↾t 𝐴 ) ) = ( 𝐽 ↾t 𝐴 ) )
6 topbas ⊢ ( 𝐽 ∈ Top → 𝐽 ∈ TopBases )
7 6 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → 𝐽 ∈ TopBases )
8 restbas ⊢ ( 𝐽 ∈ TopBases → ( 𝐽 ↾t 𝐴 ) ∈ TopBases )
9 tgcl ⊢ ( ( 𝐽 ↾t 𝐴 ) ∈ TopBases → ( topGen ‘ ( 𝐽 ↾t 𝐴 ) ) ∈ Top )
10 7 8 9 3syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( topGen ‘ ( 𝐽 ↾t 𝐴 ) ) ∈ Top )
11 5 10 eqeltrrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉 ) → ( 𝐽 ↾t 𝐴 ) ∈ Top )