Description: If K is a finer topology than J , then the subspace topologies induced by A maintain this relationship. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by Mario Carneiro, 1-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ssrest | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | |
|
2 | ssrexv | |
|
3 | 2 | ad2antlr | |
4 | n0i | |
|
5 | restfn | |
|
6 | 5 | fndmi | |
7 | 6 | ndmov | |
8 | 4 7 | nsyl2 | |
9 | 8 | adantl | |
10 | elrest | |
|
11 | 9 10 | syl | |
12 | simpll | |
|
13 | 9 | simprd | |
14 | elrest | |
|
15 | 12 13 14 | syl2anc | |
16 | 3 11 15 | 3imtr4d | |
17 | 1 16 | mpd | |
18 | 17 | ex | |
19 | 18 | ssrdv | |