Metamath Proof Explorer

Theorem resttopon2

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

Ref Expression
Assertion resttopon2 
|- ( ( J e. ( TopOn ` X ) /\ A e. V ) -> ( J |`t A ) e. ( TopOn ` ( A i^i X ) ) )

Proof

Step Hyp Ref Expression
1 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
2 resttop 
 |-  ( ( J e. Top /\ A e. V ) -> ( J |`t A ) e. Top )
3 1 2 sylan 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. V ) -> ( J |`t A ) e. Top )
4 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
5 4 ineq2d 
 |-  ( J e. ( TopOn ` X ) -> ( A i^i X ) = ( A i^i U. J ) )
6 5 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. V ) -> ( A i^i X ) = ( A i^i U. J ) )
7 eqid 
 |-  U. J = U. J
8 7 restuni2 
 |-  ( ( J e. Top /\ A e. V ) -> ( A i^i U. J ) = U. ( J |`t A ) )
9 1 8 sylan 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. V ) -> ( A i^i U. J ) = U. ( J |`t A ) )
10 6 9 eqtrd 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. V ) -> ( A i^i X ) = U. ( J |`t A ) )
11 istopon 
 |-  ( ( J |`t A ) e. ( TopOn ` ( A i^i X ) ) <-> ( ( J |`t A ) e. Top /\ ( A i^i X ) = U. ( J |`t A ) ) )
12 3 10 11 sylanbrc 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. V ) -> ( J |`t A ) e. ( TopOn ` ( A i^i X ) ) )