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	⊢ 𝐵 = ( Base ‘ 𝑊 )
	topnval.2	⊢ 𝐽 = ( TopSet ‘ 𝑊 )
Assertion	topnid	⊢ ( 𝐽 ⊆ 𝒫 𝐵 → 𝐽 = ( TopOpen ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		topnval.1	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		topnval.2	⊢ 𝐽 = ( TopSet ‘ 𝑊 )
3	1 2	topnval	⊢ ( 𝐽 ↾t 𝐵 ) = ( TopOpen ‘ 𝑊 )
4	1	fvexi	⊢ 𝐵 ∈ V
5		restid2	⊢ ( ( 𝐵 ∈ V ∧ 𝐽 ⊆ 𝒫 𝐵 ) → ( 𝐽 ↾t 𝐵 ) = 𝐽 )
6	4 5	mpan	⊢ ( 𝐽 ⊆ 𝒫 𝐵 → ( 𝐽 ↾t 𝐵 ) = 𝐽 )
7	3 6	syl5reqr	⊢ ( 𝐽 ⊆ 𝒫 𝐵 → 𝐽 = ( TopOpen ‘ 𝑊 ) )