# Metamath Proof Explorer

## Theorem resttopon

Description: A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion resttopon
`|- ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) )`

### Proof

Step Hyp Ref Expression
1 topontop
` |-  ( J e. ( TopOn ` X ) -> J e. Top )`
2 id
` |-  ( A C_ X -> A C_ X )`
3 toponmax
` |-  ( J e. ( TopOn ` X ) -> X e. J )`
4 ssexg
` |-  ( ( A C_ X /\ X e. J ) -> A e. _V )`
5 2 3 4 syl2anr
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> A e. _V )`
6 resttop
` |-  ( ( J e. Top /\ A e. _V ) -> ( J |`t A ) e. Top )`
7 1 5 6 syl2an2r
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) e. Top )`
8 simpr
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> A C_ X )`
9 sseqin2
` |-  ( A C_ X <-> ( X i^i A ) = A )`
10 8 9 sylib
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( X i^i A ) = A )`
11 simpl
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> J e. ( TopOn ` X ) )`
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> X e. J )`
13 elrestr
` |-  ( ( J e. ( TopOn ` X ) /\ A e. _V /\ X e. J ) -> ( X i^i A ) e. ( J |`t A ) )`
14 11 5 12 13 syl3anc
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( X i^i A ) e. ( J |`t A ) )`
15 10 14 eqeltrrd
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> A e. ( J |`t A ) )`
16 elssuni
` |-  ( A e. ( J |`t A ) -> A C_ U. ( J |`t A ) )`
17 15 16 syl
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> A C_ U. ( J |`t A ) )`
18 restval
` |-  ( ( J e. ( TopOn ` X ) /\ A e. _V ) -> ( J |`t A ) = ran ( x e. J |-> ( x i^i A ) ) )`
19 5 18 syldan
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) = ran ( x e. J |-> ( x i^i A ) ) )`
20 inss2
` |-  ( x i^i A ) C_ A`
21 vex
` |-  x e. _V`
22 21 inex1
` |-  ( x i^i A ) e. _V`
23 22 elpw
` |-  ( ( x i^i A ) e. ~P A <-> ( x i^i A ) C_ A )`
24 20 23 mpbir
` |-  ( x i^i A ) e. ~P A`
25 24 a1i
` |-  ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ x e. J ) -> ( x i^i A ) e. ~P A )`
26 25 fmpttd
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( x e. J |-> ( x i^i A ) ) : J --> ~P A )`
27 26 frnd
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ran ( x e. J |-> ( x i^i A ) ) C_ ~P A )`
28 19 27 eqsstrd
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) C_ ~P A )`
29 sspwuni
` |-  ( ( J |`t A ) C_ ~P A <-> U. ( J |`t A ) C_ A )`
30 28 29 sylib
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> U. ( J |`t A ) C_ A )`
31 17 30 eqssd
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> A = U. ( J |`t A ) )`
32 istopon
` |-  ( ( J |`t A ) e. ( TopOn ` A ) <-> ( ( J |`t A ) e. Top /\ A = U. ( J |`t A ) ) )`
33 7 31 32 sylanbrc
` |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) )`