Theorem topnval

Description: Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Hypotheses	topnval.1	|- B = ( Base ` W )
	topnval.2	|- J = ( TopSet ` W )
Assertion	topnval	|- ( J |`t B ) = ( TopOpen ` W )

Proof

Step	Hyp	Ref	Expression
1		topnval.1	|- B = ( Base ` W )
2		topnval.2	|- J = ( TopSet ` W )
3		fveq2	|- ( w = W -> ( TopSet ` w ) = ( TopSet ` W ) )
4	3 2	eqtr4di	|- ( w = W -> ( TopSet ` w ) = J )
5		fveq2	|- ( w = W -> ( Base ` w ) = ( Base ` W ) )
6	5 1	eqtr4di	|- ( w = W -> ( Base ` w ) = B )
7	4 6	oveq12d	|- ( w = W -> ( ( TopSet ` w ) |`t ( Base ` w ) ) = ( J |`t B ) )
8		df-topn	|- TopOpen = ( w e. _V |-> ( ( TopSet ` w ) |`t ( Base ` w ) ) )
9		ovex	|- ( J |`t B ) e. _V
10	7 8 9	fvmpt	|- ( W e. _V -> ( TopOpen ` W ) = ( J |`t B ) )
11	10	eqcomd	|- ( W e. _V -> ( J |`t B ) = ( TopOpen ` W ) )
12		0rest	|- ( (/) |`t B ) = (/)
13		fvprc	|- ( -. W e. _V -> ( TopSet ` W ) = (/) )
14	2 13	syl5eq	|- ( -. W e. _V -> J = (/) )
15	14	oveq1d	|- ( -. W e. _V -> ( J |`t B ) = ( (/) |`t B ) )
16		fvprc	|- ( -. W e. _V -> ( TopOpen ` W ) = (/) )
17	12 15 16	3eqtr4a	|- ( -. W e. _V -> ( J |`t B ) = ( TopOpen ` W ) )
18	11 17	pm2.61i	|- ( J |`t B ) = ( TopOpen ` W )