Step | Hyp | Ref
| Expression |
1 | | qtoprest.2 |
. . . . . 6
 TopOn    |
2 | | qtoprest.3 |
. . . . . . 7
       |
3 | | fofn 5795 |
. . . . . . 7
    
  |
4 | 2, 3 | syl 17 |
. . . . . 6
   |
5 | | qtopid 20720 |
. . . . . 6
  TopOn     qTop     |
6 | 1, 4, 5 | syl2anc 667 |
. . . . 5
   qTop     |
7 | | qtoprest.5 |
. . . . . . 7
        |
8 | | cnvimass 5188 |
. . . . . . . 8
    
 |
9 | | fndm 5675 |
. . . . . . . . 9
   |
10 | 4, 9 | syl 17 |
. . . . . . . 8
   |
11 | 8, 10 | syl5sseq 3480 |
. . . . . . 7
        |
12 | 7, 11 | eqsstrd 3466 |
. . . . . 6

  |
13 | | toponuni 19942 |
. . . . . . 7
 TopOn 
   |
14 | 1, 13 | syl 17 |
. . . . . 6
    |
15 | 12, 14 | sseqtrd 3468 |
. . . . 5

   |
16 | | eqid 2451 |
. . . . . 6
   |
17 | 16 | cnrest 20301 |
. . . . 5
    qTop         ↾t   qTop     |
18 | 6, 15, 17 | syl2anc 667 |
. . . 4
     ↾t   qTop     |
19 | | qtoptopon 20719 |
. . . . . 6
  TopOn        qTop  TopOn    |
20 | 1, 2, 19 | syl2anc 667 |
. . . . 5
  qTop  TopOn    |
21 | | df-ima 4847 |
. . . . . . 7
       |
22 | 7 | imaeq2d 5168 |
. . . . . . . 8
                |
23 | | qtoprest.4 |
. . . . . . . . 9

  |
24 | | foimacnv 5831 |
. . . . . . . . 9
     
            |
25 | 2, 23, 24 | syl2anc 667 |
. . . . . . . 8
            |
26 | 22, 25 | eqtrd 2485 |
. . . . . . 7
       |
27 | 21, 26 | syl5eqr 2499 |
. . . . . 6
     |
28 | | eqimss 3484 |
. . . . . 6
   
   |
29 | 27, 28 | syl 17 |
. . . . 5
     |
30 | | cnrest2 20302 |
. . . . 5
   qTop  TopOn 
 
     
↾t   qTop  
   
↾t    qTop
 ↾t      |
31 | 20, 29, 23, 30 | syl3anc 1268 |
. . . 4
     
↾t   qTop  
   
↾t    qTop
 ↾t      |
32 | 18, 31 | mpbid 214 |
. . 3
     ↾t    qTop  ↾t     |
33 | | resttopon 20177 |
. . . 4
   qTop  TopOn 

  qTop 
↾t  TopOn    |
34 | 20, 23, 33 | syl2anc 667 |
. . 3
   qTop  ↾t  TopOn    |
35 | | qtopss 20730 |
. . 3
      ↾t    qTop  ↾t     qTop  ↾t  TopOn 
  
  qTop 
↾t   
↾t  qTop      |
36 | 32, 34, 27, 35 | syl3anc 1268 |
. 2
   qTop  ↾t   
↾t  qTop      |
37 | | resttopon 20177 |
. . . . . 6
  TopOn    ↾t  TopOn    |
38 | 1, 12, 37 | syl2anc 667 |
. . . . 5
 
↾t  TopOn    |
39 | | fnfun 5673 |
. . . . . . . 8
   |
40 | 4, 39 | syl 17 |
. . . . . . 7
   |
41 | 12, 10 | sseqtr4d 3469 |
. . . . . . 7

  |
42 | | fores 5802 |
. . . . . . 7
               |
43 | 40, 41, 42 | syl2anc 667 |
. . . . . 6
             |
44 | | foeq3 5791 |
. . . . . . 7
               
         |
45 | 26, 44 | syl 17 |
. . . . . 6
                     |
46 | 43, 45 | mpbid 214 |
. . . . 5
         |
47 | | elqtop3 20718 |
. . . . 5
  
↾t  TopOn            ↾t  qTop   
        
↾t      |
48 | 38, 46, 47 | syl2anc 667 |
. . . 4
   
↾t  qTop   
        
↾t      |
49 | | cnvresima 5324 |
. . . . . . . 8
               |
50 | | imass2 5204 |
. . . . . . . . . . 11
             |
51 | 50 | adantl 468 |
. . . . . . . . . 10
 

            |
52 | 7 | adantr 467 |
. . . . . . . . . 10
 

       |
53 | 51, 52 | sseqtr4d 3469 |
. . . . . . . . 9
 

       |
54 | | df-ss 3418 |
. . . . . . . . 9
     
              |
55 | 53, 54 | sylib 200 |
. . . . . . . 8
 

              |
56 | 49, 55 | syl5eq 2497 |
. . . . . . 7
 

  
           |
57 | 56 | eleq1d 2513 |
. . . . . 6
 

         ↾t        ↾t     |
58 | | simplrl 770 |
. . . . . . . . . 10
   
      ↾t       |
59 | | df-ss 3418 |
. . . . . . . . . 10

    |
60 | 58, 59 | sylib 200 |
. . . . . . . . 9
   
      ↾t     
   |
61 | | topontop 19941 |
. . . . . . . . . . . 12
  qTop  TopOn   qTop    |
62 | 20, 61 | syl 17 |
. . . . . . . . . . 11
  qTop    |
63 | 62 | ad2antrr 732 |
. . . . . . . . . 10
   
      ↾t      qTop    |
64 | | toponmax 19943 |
. . . . . . . . . . . . . 14
 TopOn 
  |
65 | 1, 64 | syl 17 |
. . . . . . . . . . . . 13
   |
66 | | fornex 6762 |
. . . . . . . . . . . . 13
     
   |
67 | 65, 2, 66 | sylc 62 |
. . . . . . . . . . . 12
   |
68 | 67, 23 | ssexd 4550 |
. . . . . . . . . . 11
   |
69 | 68 | ad2antrr 732 |
. . . . . . . . . 10
   
      ↾t       |
70 | 23 | ad2antrr 732 |
. . . . . . . . . . . 12
   
      ↾t       |
71 | 58, 70 | sstrd 3442 |
. . . . . . . . . . 11
   
      ↾t       |
72 | | topontop 19941 |
. . . . . . . . . . . . . . . 16
 TopOn 
  |
73 | 1, 72 | syl 17 |
. . . . . . . . . . . . . . 15
   |
74 | | restopn2 20193 |
. . . . . . . . . . . . . . 15
 
        ↾t 
               |
75 | 73, 74 | sylan 474 |
. . . . . . . . . . . . . 14
 
        ↾t 
               |
76 | 75 | simprbda 629 |
. . . . . . . . . . . . 13
          ↾t  
       |
77 | 76 | adantrl 722 |
. . . . . . . . . . . 12
    
      ↾t           |
78 | 77 | an32s 813 |
. . . . . . . . . . 11
   
      ↾t            |
79 | | elqtop3 20718 |
. . . . . . . . . . . . 13
  TopOn         qTop 
          |
80 | 1, 2, 79 | syl2anc 667 |
. . . . . . . . . . . 12
   qTop 
          |
81 | 80 | ad2antrr 732 |
. . . . . . . . . . 11
   
      ↾t       qTop 
          |
82 | 71, 78, 81 | mpbir2and 933 |
. . . . . . . . . 10
   
      ↾t      qTop    |
83 | | elrestr 15327 |
. . . . . . . . . 10
   qTop   qTop  
    qTop  ↾t    |
84 | 63, 69, 82, 83 | syl3anc 1268 |
. . . . . . . . 9
   
      ↾t     
   qTop  ↾t    |
85 | 60, 84 | eqeltrrd 2530 |
. . . . . . . 8
   
      ↾t       qTop  ↾t    |
86 | 34 | ad2antrr 732 |
. . . . . . . . . . . 12
   
      ↾t           qTop
 ↾t  TopOn    |
87 | | toponuni 19942 |
. . . . . . . . . . . 12
   qTop  ↾t  TopOn     qTop 
↾t    |
88 | 86, 87 | syl 17 |
. . . . . . . . . . 11
   
      ↾t            qTop 
↾t    |
89 | 88 | difeq1d 3550 |
. . . . . . . . . 10
   
      ↾t               qTop  ↾t     |
90 | 23 | ad2antrr 732 |
. . . . . . . . . . . 12
   
      ↾t           |
91 | 20 | ad2antrr 732 |
. . . . . . . . . . . . 13
   
      ↾t          qTop  TopOn    |
92 | | toponuni 19942 |
. . . . . . . . . . . . 13
  qTop  TopOn    qTop    |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . 12
   
      ↾t           qTop    |
94 | 90, 93 | sseqtrd 3468 |
. . . . . . . . . . 11
   
      ↾t           qTop    |
95 | 90 | ssdifssd 3571 |
. . . . . . . . . . . 12
   
      ↾t             |
96 | 40 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
   
      ↾t           |
97 | | funcnvcnv 5641 |
. . . . . . . . . . . . . . 15

    |
98 | | imadif 5658 |
. . . . . . . . . . . . . . 15
  
                     |
99 | 96, 97, 98 | 3syl 18 |
. . . . . . . . . . . . . 14
   
      ↾t                              |
100 | 7 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
   
      ↾t                |
101 | 100 | difeq1d 3550 |
. . . . . . . . . . . . . 14
   
      ↾t                              |
102 | 99, 101 | eqtr4d 2488 |
. . . . . . . . . . . . 13
   
      ↾t                         |
103 | | simpr 463 |
. . . . . . . . . . . . . 14
   
      ↾t               |
104 | 38 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
   
      ↾t          ↾t  TopOn    |
105 | | toponuni 19942 |
. . . . . . . . . . . . . . . . 17
  ↾t  TopOn    ↾t    |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . 16
   
      ↾t           ↾t    |
107 | 106 | difeq1d 3550 |
. . . . . . . . . . . . . . 15
   
      ↾t                   ↾t          |
108 | | topontop 19941 |
. . . . . . . . . . . . . . . . 17
  ↾t  TopOn   ↾t    |
109 | 104, 108 | syl 17 |
. . . . . . . . . . . . . . . 16
   
      ↾t          ↾t    |
110 | | simplrr 771 |
. . . . . . . . . . . . . . . 16
   
      ↾t               ↾t    |
111 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
  ↾t   
↾t   |
112 | 111 | opncld 20048 |
. . . . . . . . . . . . . . . 16
  
↾t        ↾t      ↾t           
↾t     |
113 | 109, 110,
112 | syl2anc 667 |
. . . . . . . . . . . . . . 15
   
      ↾t           
↾t           
↾t     |
114 | 107, 113 | eqeltrd 2529 |
. . . . . . . . . . . . . 14
   
      ↾t                    ↾t     |
115 | | restcldr 20190 |
. . . . . . . . . . . . . 14
                 ↾t                 |
116 | 103, 114,
115 | syl2anc 667 |
. . . . . . . . . . . . 13
   
      ↾t                      |
117 | 102, 116 | eqeltrd 2529 |
. . . . . . . . . . . 12
   
      ↾t                      |
118 | | qtopcld 20728 |
. . . . . . . . . . . . . 14
  TopOn              qTop                     |
119 | 1, 2, 118 | syl2anc 667 |
. . . . . . . . . . . . 13
        qTop  
                  |
120 | 119 | ad2antrr 732 |
. . . . . . . . . . . 12
   
      ↾t                qTop                     |
121 | 95, 117, 120 | mpbir2and 933 |
. . . . . . . . . . 11
   
      ↾t               qTop     |
122 | | difssd 3561 |
. . . . . . . . . . 11
   
      ↾t             |
123 | | eqid 2451 |
. . . . . . . . . . . 12
  qTop   
qTop   |
124 | 123 | restcldi 20189 |
. . . . . . . . . . 11
 
  qTop        qTop   

        qTop  ↾t     |
125 | 94, 121, 122, 124 | syl3anc 1268 |
. . . . . . . . . 10
   
      ↾t                qTop
 ↾t     |
126 | 89, 125 | eqeltrrd 2530 |
. . . . . . . . 9
   
      ↾t             qTop  ↾t        qTop  ↾t     |
127 | | topontop 19941 |
. . . . . . . . . . 11
   qTop  ↾t  TopOn    qTop
 ↾t    |
128 | 86, 127 | syl 17 |
. . . . . . . . . 10
   
      ↾t           qTop
 ↾t    |
129 | | simplrl 770 |
. . . . . . . . . . 11
   
      ↾t           |
130 | 129, 88 | sseqtrd 3468 |
. . . . . . . . . 10
   
      ↾t            qTop 
↾t    |
131 | | eqid 2451 |
. . . . . . . . . . 11
   qTop
 ↾t     qTop
 ↾t   |
132 | 131 | isopn2 20047 |
. . . . . . . . . 10
    qTop  ↾t 
   qTop
 ↾t      qTop  ↾t      qTop  ↾t        qTop
 ↾t      |
133 | 128, 130,
132 | syl2anc 667 |
. . . . . . . . 9
   
      ↾t            qTop  ↾t      qTop  ↾t        qTop
 ↾t      |
134 | 126, 133 | mpbird 236 |
. . . . . . . 8
   
      ↾t           qTop  ↾t    |
135 | | qtoprest.6 |
. . . . . . . . 9
 
       |
136 | 135 | adantr 467 |
. . . . . . . 8
 
       ↾t    
       |
137 | 85, 134, 136 | mpjaodan 795 |
. . . . . . 7
 
       ↾t      qTop  ↾t    |
138 | 137 | expr 620 |
. . . . . 6
 

       ↾t    qTop  ↾t     |
139 | 57, 138 | sylbid 219 |
. . . . 5
 

         ↾t 
  qTop  ↾t     |
140 | 139 | expimpd 608 |
. . . 4
     
    
↾t  
  qTop 
↾t     |
141 | 48, 140 | sylbid 219 |
. . 3
   
↾t  qTop   
  qTop 
↾t     |
142 | 141 | ssrdv 3438 |
. 2
   ↾t  qTop   
  qTop 
↾t    |
143 | 36, 142 | eqssd 3449 |
1
   qTop  ↾t   
↾t  qTop      |