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 K V J K J 𝑡 A K 𝑡 A

Proof

Step Hyp Ref Expression
1 simpr K V J K x J 𝑡 A x J 𝑡 A
2 ssrexv J K y J x = y A y K x = y A
3 2 ad2antlr K V J K x J 𝑡 A y J x = y A y K x = y A
4 n0i x J 𝑡 A ¬ J 𝑡 A =
5 restfn 𝑡 Fn V × V
6 fndm 𝑡 Fn V × V dom 𝑡 = V × V
7 5 6 ax-mp dom 𝑡 = V × V
8 7 ndmov ¬ J V A V J 𝑡 A =
9 4 8 nsyl2 x J 𝑡 A J V A V
10 9 adantl K V J K x J 𝑡 A J V A V
11 elrest J V A V x J 𝑡 A y J x = y A
12 10 11 syl K V J K x J 𝑡 A x J 𝑡 A y J x = y A
13 simpll K V J K x J 𝑡 A K V
14 10 simprd K V J K x J 𝑡 A A V
15 elrest K V A V x K 𝑡 A y K x = y A
16 13 14 15 syl2anc K V J K x J 𝑡 A x K 𝑡 A y K x = y A
17 3 12 16 3imtr4d K V J K x J 𝑡 A x J 𝑡 A x K 𝑡 A
18 1 17 mpd K V J K x J 𝑡 A x K 𝑡 A
19 18 ex K V J K x J 𝑡 A x K 𝑡 A
20 19 ssrdv K V J K J 𝑡 A K 𝑡 A