Theorem restuni

Description: The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Hypothesis	restuni.1	|- X = U. J
Assertion	restuni	|- ( ( J e. Top /\ A C_ X ) -> A = U. ( J |`t A ) )

Proof

Step	Hyp	Ref	Expression
1		restuni.1	|- X = U. J
2	1	toptopon	|- ( J e. Top <-> J e. ( TopOn ` X ) )
3		resttopon	|- ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) )
4	2 3	sylanb	|- ( ( J e. Top /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) )
5		toponuni	|- ( ( J |`t A ) e. ( TopOn ` A ) -> A = U. ( J |`t A ) )
6	4 5	syl	|- ( ( J e. Top /\ A C_ X ) -> A = U. ( J |`t A ) )