Metamath Proof Explorer

Theorem resstopn

Description: The topology of a restricted structure. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses resstopn.1 
|- H = ( K |`s A )
resstopn.2 
|- J = ( TopOpen ` K )
Assertion resstopn 
|- ( J |`t A ) = ( TopOpen ` H )

Proof

Step Hyp Ref Expression
1 resstopn.1 
 |-  H = ( K |`s A )
2 resstopn.2 
 |-  J = ( TopOpen ` K )
3 fvex 
 |-  ( TopSet ` K ) e. _V
4 fvex 
 |-  ( Base ` K ) e. _V
5 restco 
 |-  ( ( ( TopSet ` K ) e. _V /\ ( Base ` K ) e. _V /\ A e. _V ) -> ( ( ( TopSet ` K ) |`t ( Base ` K ) ) |`t A ) = ( ( TopSet ` K ) |`t ( ( Base ` K ) i^i A ) ) )
6 3 4 5 mp3an12 
 |-  ( A e. _V -> ( ( ( TopSet ` K ) |`t ( Base ` K ) ) |`t A ) = ( ( TopSet ` K ) |`t ( ( Base ` K ) i^i A ) ) )
7 eqid 
 |-  ( TopSet ` K ) = ( TopSet ` K )
8 1 7 resstset 
 |-  ( A e. _V -> ( TopSet ` K ) = ( TopSet ` H ) )
9 incom 
 |-  ( ( Base ` K ) i^i A ) = ( A i^i ( Base ` K ) )
10 eqid 
 |-  ( Base ` K ) = ( Base ` K )
11 1 10 ressbas 
 |-  ( A e. _V -> ( A i^i ( Base ` K ) ) = ( Base ` H ) )
12 9 11 syl5eq 
 |-  ( A e. _V -> ( ( Base ` K ) i^i A ) = ( Base ` H ) )
13 8 12 oveq12d 
 |-  ( A e. _V -> ( ( TopSet ` K ) |`t ( ( Base ` K ) i^i A ) ) = ( ( TopSet ` H ) |`t ( Base ` H ) ) )
14 6 13 eqtrd 
 |-  ( A e. _V -> ( ( ( TopSet ` K ) |`t ( Base ` K ) ) |`t A ) = ( ( TopSet ` H ) |`t ( Base ` H ) ) )
15 10 7 topnval 
 |-  ( ( TopSet ` K ) |`t ( Base ` K ) ) = ( TopOpen ` K )
16 15 2 eqtr4i 
 |-  ( ( TopSet ` K ) |`t ( Base ` K ) ) = J
17 16 oveq1i 
 |-  ( ( ( TopSet ` K ) |`t ( Base ` K ) ) |`t A ) = ( J |`t A )
18 eqid 
 |-  ( Base ` H ) = ( Base ` H )
19 eqid 
 |-  ( TopSet ` H ) = ( TopSet ` H )
20 18 19 topnval 
 |-  ( ( TopSet ` H ) |`t ( Base ` H ) ) = ( TopOpen ` H )
21 14 17 20 3eqtr3g 
 |-  ( A e. _V -> ( J |`t A ) = ( TopOpen ` H ) )
22 simpr 
 |-  ( ( J e. _V /\ A e. _V ) -> A e. _V )
23 restfn 
 |-  |`t Fn ( _V X. _V )
24 23 fndmi 
 |-  dom |`t = ( _V X. _V )
25 24 ndmov 
 |-  ( -. ( J e. _V /\ A e. _V ) -> ( J |`t A ) = (/) )
26 22 25 nsyl5 
 |-  ( -. A e. _V -> ( J |`t A ) = (/) )
27 reldmress 
 |-  Rel dom |`s
28 27 ovprc2 
 |-  ( -. A e. _V -> ( K |`s A ) = (/) )
29 1 28 syl5eq 
 |-  ( -. A e. _V -> H = (/) )
30 29 fveq2d 
 |-  ( -. A e. _V -> ( TopSet ` H ) = ( TopSet ` (/) ) )
31 tsetid 
 |-  TopSet = Slot ( TopSet ` ndx )
32 31 str0 
 |-  (/) = ( TopSet ` (/) )
33 30 32 eqtr4di 
 |-  ( -. A e. _V -> ( TopSet ` H ) = (/) )
34 33 oveq1d 
 |-  ( -. A e. _V -> ( ( TopSet ` H ) |`t ( Base ` H ) ) = ( (/) |`t ( Base ` H ) ) )
35 0rest 
 |-  ( (/) |`t ( Base ` H ) ) = (/)
36 34 20 35 3eqtr3g 
 |-  ( -. A e. _V -> ( TopOpen ` H ) = (/) )
37 26 36 eqtr4d 
 |-  ( -. A e. _V -> ( J |`t A ) = ( TopOpen ` H ) )
38 21 37 pm2.61i 
 |-  ( J |`t A ) = ( TopOpen ` H )