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

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 sseqin2 
 |-  ( A C_ X <-> ( X i^i A ) = A )
9 8 bilani 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( X i^i A ) = A )
10 simpl 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> J e. ( TopOn ` X ) )
11 3 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> X e. J )
12 elrestr 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. _V /\ X e. J ) -> ( X i^i A ) e. ( J |`t A ) )
13 10 5 11 12 syl3anc 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( X i^i A ) e. ( J |`t A ) )
14 9 13 eqeltrrd 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> A e. ( J |`t A ) )
15 elssuni 
 |-  ( A e. ( J |`t A ) -> A C_ U. ( J |`t A ) )
16 14 15 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> A C_ U. ( J |`t A ) )
17 restval 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. _V ) -> ( J |`t A ) = ran ( x e. J |-> ( x i^i A ) ) )
18 5 17 syldan 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) = ran ( x e. J |-> ( x i^i A ) ) )
19 inss2 
 |-  ( x i^i A ) C_ A
20 vex 
 |-  x e. _V
21 20 inex1 
 |-  ( x i^i A ) e. _V
22 21 elpw 
 |-  ( ( x i^i A ) e. ~P A <-> ( x i^i A ) C_ A )
23 19 22 mpbir 
 |-  ( x i^i A ) e. ~P A
24 23 a1i 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ x e. J ) -> ( x i^i A ) e. ~P A )
25 24 fmpttd 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( x e. J |-> ( x i^i A ) ) : J --> ~P A )
26 25 frnd 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ran ( x e. J |-> ( x i^i A ) ) C_ ~P A )
27 18 26 eqsstrd 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) C_ ~P A )
28 sspwuni 
 |-  ( ( J |`t A ) C_ ~P A <-> U. ( J |`t A ) C_ A )
29 27 28 sylib 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> U. ( J |`t A ) C_ A )
30 16 29 eqssd 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> A = U. ( J |`t A ) )
31 istopon 
 |-  ( ( J |`t A ) e. ( TopOn ` A ) <-> ( ( J |`t A ) e. Top /\ A = U. ( J |`t A ) ) )
32 7 30 31 sylanbrc 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) )