Metamath Proof Explorer


Theorem ssrest

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 KVJKJ𝑡AK𝑡A

Proof

Step Hyp Ref Expression
1 simpr KVJKxJ𝑡AxJ𝑡A
2 ssrexv JKyJx=yAyKx=yA
3 2 ad2antlr KVJKxJ𝑡AyJx=yAyKx=yA
4 n0i xJ𝑡A¬J𝑡A=
5 restfn 𝑡FnV×V
6 5 fndmi dom𝑡=V×V
7 6 ndmov ¬JVAVJ𝑡A=
8 4 7 nsyl2 xJ𝑡AJVAV
9 8 adantl KVJKxJ𝑡AJVAV
10 elrest JVAVxJ𝑡AyJx=yA
11 9 10 syl KVJKxJ𝑡AxJ𝑡AyJx=yA
12 simpll KVJKxJ𝑡AKV
13 9 simprd KVJKxJ𝑡AAV
14 elrest KVAVxK𝑡AyKx=yA
15 12 13 14 syl2anc KVJKxJ𝑡AxK𝑡AyKx=yA
16 3 11 15 3imtr4d KVJKxJ𝑡AxJ𝑡AxK𝑡A
17 1 16 mpd KVJKxJ𝑡AxK𝑡A
18 17 ex KVJKxJ𝑡AxK𝑡A
19 18 ssrdv KVJKJ𝑡AK𝑡A