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 ) )
12 3 adantr 
 |-  ( ( 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 ) )