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 C_ ~P B -> J = ( TopOpen ` W ) )

Proof

Step	Hyp	Ref	Expression
1		topnval.1	|- B = ( Base ` W )
2		topnval.2	|- J = ( TopSet ` W )
3	1	fvexi	|- B e. _V
4		restid2	|- ( ( B e. _V /\ J C_ ~P B ) -> ( J |`t B ) = J )
5	3 4	mpan	|- ( J C_ ~P B -> ( J |`t B ) = J )
6	1 2	topnval	|- ( J |`t B ) = ( TopOpen ` W )
7	5 6	eqtr3di	|- ( J C_ ~P B -> J = ( TopOpen ` W ) )