Metamath Proof Explorer


Theorem restuni2

Description: The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis restin.1
|- X = U. J
Assertion restuni2
|- ( ( J e. Top /\ A e. V ) -> ( A i^i X ) = U. ( J |`t A ) )

Proof

Step Hyp Ref Expression
1 restin.1
 |-  X = U. J
2 simpl
 |-  ( ( J e. Top /\ A e. V ) -> J e. Top )
3 inss2
 |-  ( A i^i X ) C_ X
4 1 restuni
 |-  ( ( J e. Top /\ ( A i^i X ) C_ X ) -> ( A i^i X ) = U. ( J |`t ( A i^i X ) ) )
5 2 3 4 sylancl
 |-  ( ( J e. Top /\ A e. V ) -> ( A i^i X ) = U. ( J |`t ( A i^i X ) ) )
6 1 restin
 |-  ( ( J e. Top /\ A e. V ) -> ( J |`t A ) = ( J |`t ( A i^i X ) ) )
7 6 unieqd
 |-  ( ( J e. Top /\ A e. V ) -> U. ( J |`t A ) = U. ( J |`t ( A i^i X ) ) )
8 5 7 eqtr4d
 |-  ( ( J e. Top /\ A e. V ) -> ( A i^i X ) = U. ( J |`t A ) )