Theorem restrcl

Description: Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 1-May-2015)

	Ref	Expression
Assertion	restrcl	|- ( ( J |`t A ) e. Top -> ( J e. _V /\ A e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		0opn	|- ( ( J |`t A ) e. Top -> (/) e. ( J |`t A ) )
2		n0i	|- ( (/) e. ( J |`t A ) -> -. ( J |`t A ) = (/) )
3	1 2	syl	|- ( ( J |`t A ) e. Top -> -. ( J |`t A ) = (/) )
4		restfn	|- |`t Fn ( _V X. _V )
5	4	fndmi	|- dom |`t = ( _V X. _V )
6	5	ndmov	|- ( -. ( J e. _V /\ A e. _V ) -> ( J |`t A ) = (/) )
7	3 6	nsyl2	|- ( ( J |`t A ) e. Top -> ( J e. _V /\ A e. _V ) )