Step | Hyp | Ref
| Expression |
1 | | qtoprest.2 |
. . . . . 6
TopOn |
2 | | qtoprest.3 |
. . . . . . 7
|
3 | | fofn 6117 |
. . . . . . 7
|
4 | 2, 3 | syl 17 |
. . . . . 6
|
5 | | qtopid 21508 |
. . . . . 6
TopOn qTop |
6 | 1, 4, 5 | syl2anc 693 |
. . . . 5
qTop |
7 | | qtoprest.5 |
. . . . . . 7
|
8 | | cnvimass 5485 |
. . . . . . . 8
|
9 | | fndm 5990 |
. . . . . . . . 9
|
10 | 4, 9 | syl 17 |
. . . . . . . 8
|
11 | 8, 10 | syl5sseq 3653 |
. . . . . . 7
|
12 | 7, 11 | eqsstrd 3639 |
. . . . . 6
|
13 | | toponuni 20719 |
. . . . . . 7
TopOn
|
14 | 1, 13 | syl 17 |
. . . . . 6
|
15 | 12, 14 | sseqtrd 3641 |
. . . . 5
|
16 | | eqid 2622 |
. . . . . 6
|
17 | 16 | cnrest 21089 |
. . . . 5
qTop ↾t qTop |
18 | 6, 15, 17 | syl2anc 693 |
. . . 4
↾t qTop |
19 | | qtoptopon 21507 |
. . . . . 6
TopOn qTop TopOn |
20 | 1, 2, 19 | syl2anc 693 |
. . . . 5
qTop TopOn |
21 | | df-ima 5127 |
. . . . . . 7
|
22 | 7 | imaeq2d 5466 |
. . . . . . . 8
|
23 | | qtoprest.4 |
. . . . . . . . 9
|
24 | | foimacnv 6154 |
. . . . . . . . 9
|
25 | 2, 23, 24 | syl2anc 693 |
. . . . . . . 8
|
26 | 22, 25 | eqtrd 2656 |
. . . . . . 7
|
27 | 21, 26 | syl5eqr 2670 |
. . . . . 6
|
28 | | eqimss 3657 |
. . . . . 6
|
29 | 27, 28 | syl 17 |
. . . . 5
|
30 | | cnrest2 21090 |
. . . . 5
qTop TopOn
↾t qTop
↾t qTop
↾t |
31 | 20, 29, 23, 30 | syl3anc 1326 |
. . . 4
↾t qTop
↾t qTop
↾t |
32 | 18, 31 | mpbid 222 |
. . 3
↾t qTop ↾t |
33 | | resttopon 20965 |
. . . 4
qTop TopOn
qTop
↾t TopOn |
34 | 20, 23, 33 | syl2anc 693 |
. . 3
qTop ↾t TopOn |
35 | | qtopss 21518 |
. . 3
↾t qTop ↾t qTop ↾t TopOn
qTop
↾t
↾t qTop |
36 | 32, 34, 27, 35 | syl3anc 1326 |
. 2
qTop ↾t
↾t qTop |
37 | | resttopon 20965 |
. . . . . 6
TopOn ↾t TopOn |
38 | 1, 12, 37 | syl2anc 693 |
. . . . 5
↾t TopOn |
39 | | fnfun 5988 |
. . . . . . . 8
|
40 | 4, 39 | syl 17 |
. . . . . . 7
|
41 | 12, 10 | sseqtr4d 3642 |
. . . . . . 7
|
42 | | fores 6124 |
. . . . . . 7
|
43 | 40, 41, 42 | syl2anc 693 |
. . . . . 6
|
44 | | foeq3 6113 |
. . . . . . 7
|
45 | 26, 44 | syl 17 |
. . . . . 6
|
46 | 43, 45 | mpbid 222 |
. . . . 5
|
47 | | elqtop3 21506 |
. . . . 5
↾t TopOn ↾t qTop
↾t |
48 | 38, 46, 47 | syl2anc 693 |
. . . 4
↾t qTop
↾t |
49 | | cnvresima 5623 |
. . . . . . . 8
|
50 | | imass2 5501 |
. . . . . . . . . . 11
|
51 | 50 | adantl 482 |
. . . . . . . . . 10
|
52 | 7 | adantr 481 |
. . . . . . . . . 10
|
53 | 51, 52 | sseqtr4d 3642 |
. . . . . . . . 9
|
54 | | df-ss 3588 |
. . . . . . . . 9
|
55 | 53, 54 | sylib 208 |
. . . . . . . 8
|
56 | 49, 55 | syl5eq 2668 |
. . . . . . 7
|
57 | 56 | eleq1d 2686 |
. . . . . 6
↾t ↾t |
58 | | simplrl 800 |
. . . . . . . . . 10
↾t |
59 | | df-ss 3588 |
. . . . . . . . . 10
|
60 | 58, 59 | sylib 208 |
. . . . . . . . 9
↾t
|
61 | | topontop 20718 |
. . . . . . . . . . . 12
qTop TopOn qTop |
62 | 20, 61 | syl 17 |
. . . . . . . . . . 11
qTop |
63 | 62 | ad2antrr 762 |
. . . . . . . . . 10
↾t qTop |
64 | | toponmax 20730 |
. . . . . . . . . . . . . 14
TopOn
|
65 | 1, 64 | syl 17 |
. . . . . . . . . . . . 13
|
66 | | fornex 7135 |
. . . . . . . . . . . . 13
|
67 | 65, 2, 66 | sylc 65 |
. . . . . . . . . . . 12
|
68 | 67, 23 | ssexd 4805 |
. . . . . . . . . . 11
|
69 | 68 | ad2antrr 762 |
. . . . . . . . . 10
↾t |
70 | 23 | ad2antrr 762 |
. . . . . . . . . . . 12
↾t |
71 | 58, 70 | sstrd 3613 |
. . . . . . . . . . 11
↾t |
72 | | topontop 20718 |
. . . . . . . . . . . . . . . 16
TopOn
|
73 | 1, 72 | syl 17 |
. . . . . . . . . . . . . . 15
|
74 | | restopn2 20981 |
. . . . . . . . . . . . . . 15
↾t
|
75 | 73, 74 | sylan 488 |
. . . . . . . . . . . . . 14
↾t
|
76 | 75 | simprbda 653 |
. . . . . . . . . . . . 13
↾t
|
77 | 76 | adantrl 752 |
. . . . . . . . . . . 12
↾t |
78 | 77 | an32s 846 |
. . . . . . . . . . 11
↾t |
79 | | elqtop3 21506 |
. . . . . . . . . . . . 13
TopOn qTop
|
80 | 1, 2, 79 | syl2anc 693 |
. . . . . . . . . . . 12
qTop
|
81 | 80 | ad2antrr 762 |
. . . . . . . . . . 11
↾t qTop
|
82 | 71, 78, 81 | mpbir2and 957 |
. . . . . . . . . 10
↾t qTop |
83 | | elrestr 16089 |
. . . . . . . . . 10
qTop qTop
qTop ↾t |
84 | 63, 69, 82, 83 | syl3anc 1326 |
. . . . . . . . 9
↾t
qTop ↾t |
85 | 60, 84 | eqeltrrd 2702 |
. . . . . . . 8
↾t qTop ↾t |
86 | 34 | ad2antrr 762 |
. . . . . . . . . . . 12
↾t qTop
↾t TopOn |
87 | | toponuni 20719 |
. . . . . . . . . . . 12
qTop ↾t TopOn qTop
↾t |
88 | 86, 87 | syl 17 |
. . . . . . . . . . 11
↾t qTop
↾t |
89 | 88 | difeq1d 3727 |
. . . . . . . . . 10
↾t qTop ↾t |
90 | 23 | ad2antrr 762 |
. . . . . . . . . . . 12
↾t |
91 | 20 | ad2antrr 762 |
. . . . . . . . . . . . 13
↾t qTop TopOn |
92 | | toponuni 20719 |
. . . . . . . . . . . . 13
qTop TopOn qTop |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . 12
↾t qTop |
94 | 90, 93 | sseqtrd 3641 |
. . . . . . . . . . 11
↾t qTop |
95 | 90 | ssdifssd 3748 |
. . . . . . . . . . . 12
↾t |
96 | 40 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
↾t |
97 | | funcnvcnv 5956 |
. . . . . . . . . . . . . . 15
|
98 | | imadif 5973 |
. . . . . . . . . . . . . . 15
|
99 | 96, 97, 98 | 3syl 18 |
. . . . . . . . . . . . . 14
↾t |
100 | 7 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
↾t |
101 | 100 | difeq1d 3727 |
. . . . . . . . . . . . . 14
↾t |
102 | 99, 101 | eqtr4d 2659 |
. . . . . . . . . . . . 13
↾t |
103 | | simpr 477 |
. . . . . . . . . . . . . 14
↾t |
104 | 38 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
↾t ↾t TopOn |
105 | | toponuni 20719 |
. . . . . . . . . . . . . . . . 17
↾t TopOn ↾t |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . 16
↾t ↾t |
107 | 106 | difeq1d 3727 |
. . . . . . . . . . . . . . 15
↾t ↾t |
108 | | topontop 20718 |
. . . . . . . . . . . . . . . . 17
↾t TopOn ↾t |
109 | 104, 108 | syl 17 |
. . . . . . . . . . . . . . . 16
↾t ↾t |
110 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
↾t ↾t |
111 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
↾t
↾t |
112 | 111 | opncld 20837 |
. . . . . . . . . . . . . . . 16
↾t ↾t ↾t
↾t |
113 | 109, 110,
112 | syl2anc 693 |
. . . . . . . . . . . . . . 15
↾t
↾t
↾t |
114 | 107, 113 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
↾t ↾t |
115 | | restcldr 20978 |
. . . . . . . . . . . . . 14
↾t |
116 | 103, 114,
115 | syl2anc 693 |
. . . . . . . . . . . . 13
↾t |
117 | 102, 116 | eqeltrd 2701 |
. . . . . . . . . . . 12
↾t |
118 | | qtopcld 21516 |
. . . . . . . . . . . . . 14
TopOn qTop |
119 | 1, 2, 118 | syl2anc 693 |
. . . . . . . . . . . . 13
qTop
|
120 | 119 | ad2antrr 762 |
. . . . . . . . . . . 12
↾t qTop |
121 | 95, 117, 120 | mpbir2and 957 |
. . . . . . . . . . 11
↾t qTop |
122 | | difssd 3738 |
. . . . . . . . . . 11
↾t |
123 | | eqid 2622 |
. . . . . . . . . . . 12
qTop
qTop |
124 | 123 | restcldi 20977 |
. . . . . . . . . . 11
qTop qTop
qTop ↾t |
125 | 94, 121, 122, 124 | syl3anc 1326 |
. . . . . . . . . 10
↾t qTop
↾t |
126 | 89, 125 | eqeltrrd 2702 |
. . . . . . . . 9
↾t qTop ↾t qTop ↾t |
127 | | topontop 20718 |
. . . . . . . . . . 11
qTop ↾t TopOn qTop
↾t |
128 | 86, 127 | syl 17 |
. . . . . . . . . 10
↾t qTop
↾t |
129 | | simplrl 800 |
. . . . . . . . . . 11
↾t |
130 | 129, 88 | sseqtrd 3641 |
. . . . . . . . . 10
↾t qTop
↾t |
131 | | eqid 2622 |
. . . . . . . . . . 11
qTop
↾t qTop
↾t |
132 | 131 | isopn2 20836 |
. . . . . . . . . 10
qTop ↾t
qTop
↾t qTop ↾t qTop ↾t qTop
↾t |
133 | 128, 130,
132 | syl2anc 693 |
. . . . . . . . 9
↾t qTop ↾t qTop ↾t qTop
↾t |
134 | 126, 133 | mpbird 247 |
. . . . . . . 8
↾t qTop ↾t |
135 | | qtoprest.6 |
. . . . . . . . 9
|
136 | 135 | adantr 481 |
. . . . . . . 8
↾t
|
137 | 85, 134, 136 | mpjaodan 827 |
. . . . . . 7
↾t qTop ↾t |
138 | 137 | expr 643 |
. . . . . 6
↾t qTop ↾t |
139 | 57, 138 | sylbid 230 |
. . . . 5
↾t
qTop ↾t |
140 | 139 | expimpd 629 |
. . . 4
↾t
qTop
↾t |
141 | 48, 140 | sylbid 230 |
. . 3
↾t qTop
qTop
↾t |
142 | 141 | ssrdv 3609 |
. 2
↾t qTop
qTop
↾t |
143 | 36, 142 | eqssd 3620 |
1
qTop ↾t
↾t qTop |