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={\mathrm{Base}}_W$$
	topnval.2	$$⊢J=\mathrm{TopSet}\left(W\right)$$
Assertion	topnid	$$⊢J\subseteq 𝒫B\to J=\mathrm{TopOpen}\left(W\right)$$

Proof

Step	Hyp	Ref	Expression
1		topnval.1	$$⊢B={\mathrm{Base}}_W$$
2		topnval.2	$$⊢J=\mathrm{TopSet}\left(W\right)$$
3	1 2	topnval	$$⊢J{\upharpoonright }_{𝑡}B=\mathrm{TopOpen}\left(W\right)$$
4	1	fvexi	$$⊢B\in \mathrm{V}$$
5		restid2	$$⊢\left(B\in \mathrm{V}\wedge J\subseteq 𝒫B\right)\to J{\upharpoonright }_{𝑡}B=J$$
6	4 5	mpan	$$⊢J\subseteq 𝒫B\to J{\upharpoonright }_{𝑡}B=J$$
7	3 6	syl5reqr	$$⊢J\subseteq 𝒫B\to J=\mathrm{TopOpen}\left(W\right)$$