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

Metamath Proof Explorer

Theorem topnid

Description: Value of the topology extractor function when the topology is defined over the same set as the base. (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Hypotheses	topnval.1	$⊢ B = {Base}_{W}$
	topnval.2	$⊢ J = TopSet (W)$
Assertion	topnid	$⊢ J \subseteq 𝒫 B \to J = TopOpen (W)$

Proof

Step	Hyp	Ref	Expression
1		topnval.1	$⊢ B = {Base}_{W}$
2		topnval.2	$⊢ J = TopSet (W)$
3	1	fvexi	$⊢ B \in V$
4		restid2	$⊢ (B \in V \land J \subseteq 𝒫 B) \to J ↾_{𝑡} B = J$
5	3 4	mpan	$⊢ J \subseteq 𝒫 B \to J ↾_{𝑡} B = J$
6	1 2	topnval	$⊢ J ↾_{𝑡} B = TopOpen (W)$
7	5 6	eqtr3di	$⊢ J \subseteq 𝒫 B \to J = TopOpen (W)$