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 \in Top \land A \in V) \to J ↾_{𝑡} A \in Top$

Proof

Step	Hyp	Ref	Expression
1		tgrest	$⊢ (J \in Top \land A \in V) \to topGen (J ↾_{𝑡} A) = topGen (J) ↾_{𝑡} A$
2		tgtop	$⊢ J \in Top \to topGen (J) = J$
3	2	adantr	$⊢ (J \in Top \land A \in V) \to topGen (J) = J$
4	3	oveq1d	$⊢ (J \in Top \land A \in V) \to topGen (J) ↾_{𝑡} A = J ↾_{𝑡} A$
5	1 4	eqtrd	$⊢ (J \in Top \land A \in V) \to topGen (J ↾_{𝑡} A) = J ↾_{𝑡} A$
6		topbas	$⊢ J \in Top \to J \in TopBases$
7	6	adantr	$⊢ (J \in Top \land A \in V) \to J \in TopBases$
8		restbas	$⊢ J \in TopBases \to J ↾_{𝑡} A \in TopBases$
9		tgcl	$⊢ J ↾_{𝑡} A \in TopBases \to topGen (J ↾_{𝑡} A) \in Top$
10	7 8 9	3syl	$⊢ (J \in Top \land A \in V) \to topGen (J ↾_{𝑡} A) \in Top$
11	5 10	eqeltrrd	$⊢ (J \in Top \land A \in V) \to J ↾_{𝑡} A \in Top$