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