Metamath Proof Explorer


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 ) )