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 2	topnval	|- ( J |`t B ) = ( TopOpen ` W )
4	1	fvexi	|- B e. _V
5		restid2	|- ( ( B e. _V /\ J C_ ~P B ) -> ( J |`t B ) = J )
6	4 5	mpan	|- ( J C_ ~P B -> ( J |`t B ) = J )
7	3 6	syl5reqr	|- ( J C_ ~P B -> J = ( TopOpen ` W ) )