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 𝑠 A
resstopn.2 J = TopOpen K
Assertion resstopn J 𝑡 A = TopOpen H

Proof

Step Hyp Ref Expression
1 resstopn.1 H = K 𝑠 A
2 resstopn.2 J = TopOpen K
3 fvex TopSet K V
4 fvex Base K V
5 restco TopSet K V Base K V A V TopSet K 𝑡 Base K 𝑡 A = TopSet K 𝑡 Base K A
6 3 4 5 mp3an12 A V TopSet K 𝑡 Base K 𝑡 A = TopSet K 𝑡 Base K A
7 eqid TopSet K = TopSet K
8 1 7 resstset A V TopSet K = TopSet H
9 incom Base K A = A Base K
10 eqid Base K = Base K
11 1 10 ressbas A V A Base K = Base H
12 9 11 syl5eq A V Base K A = Base H
13 8 12 oveq12d A V TopSet K 𝑡 Base K A = TopSet H 𝑡 Base H
14 6 13 eqtrd A V TopSet K 𝑡 Base K 𝑡 A = TopSet H 𝑡 Base H
15 10 7 topnval TopSet K 𝑡 Base K = TopOpen K
16 15 2 eqtr4i TopSet K 𝑡 Base K = J
17 16 oveq1i TopSet K 𝑡 Base K 𝑡 A = J 𝑡 A
18 eqid Base H = Base H
19 eqid TopSet H = TopSet H
20 18 19 topnval TopSet H 𝑡 Base H = TopOpen H
21 14 17 20 3eqtr3g A V J 𝑡 A = TopOpen H
22 simpr J V A V A V
23 22 con3i ¬ A V ¬ J V A V
24 restfn 𝑡 Fn V × V
25 fndm 𝑡 Fn V × V dom 𝑡 = V × V
26 24 25 ax-mp dom 𝑡 = V × V
27 26 ndmov ¬ J V A V J 𝑡 A =
28 23 27 syl ¬ A V J 𝑡 A =
29 reldmress Rel dom 𝑠
30 29 ovprc2 ¬ A V K 𝑠 A =
31 1 30 syl5eq ¬ A V H =
32 31 fveq2d ¬ A V TopSet H = TopSet
33 df-tset TopSet = Slot 9
34 33 str0 = TopSet
35 32 34 syl6eqr ¬ A V TopSet H =
36 35 oveq1d ¬ A V TopSet H 𝑡 Base H = 𝑡 Base H
37 0rest 𝑡 Base H =
38 36 20 37 3eqtr3g ¬ A V TopOpen H =
39 28 38 eqtr4d ¬ A V J 𝑡 A = TopOpen H
40 21 39 pm2.61i J 𝑡 A = TopOpen H