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 )