This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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