Step | Hyp | Ref
| Expression |
1 | | f1ocnv 5826 |
. . . . . . . . 9
    
       |
2 | | f1ofun 5816 |
. . . . . . . . 9
         |
3 | 1, 2 | syl 17 |
. . . . . . . 8
    
   |
4 | 3 | ad2antlr 733 |
. . . . . . 7
            |
5 | | simpr 463 |
. . . . . . . 8
           |
6 | | df-rn 4845 |
. . . . . . . . 9
  |
7 | | f1ofo 5821 |
. . . . . . . . . . 11
    
      |
8 | 7 | ad2antlr 733 |
. . . . . . . . . 10
               |
9 | | forn 5796 |
. . . . . . . . . 10
       |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
           |
11 | 6, 10 | syl5eqr 2499 |
. . . . . . . 8
            |
12 | 5, 11 | sseqtr4d 3469 |
. . . . . . 7
            |
13 | | funimass4 5916 |
. . . . . . 7
    
              

                 |
14 | 4, 12, 13 | syl2anc 667 |
. . . . . 6
                                          |
15 | | dfss3 3422 |
. . . . . . 7
    qTop   

   qTop 
    |
16 | | inss1 3652 |
. . . . . . . . . . . . . . . 16
  qTop    
qTop   |
17 | | simprl 764 |
. . . . . . . . . . . . . . . 16
    
          qTop   
 
  qTop 
    |
18 | 16, 17 | sseldi 3430 |
. . . . . . . . . . . . . . 15
    
          qTop   
 

qTop    |
19 | | qtopcmp.1 |
. . . . . . . . . . . . . . . . . 18
  |
20 | 19 | elqtop2 20716 |
. . . . . . . . . . . . . . . . 17
         qTop 
          |
21 | 7, 20 | sylan2 477 |
. . . . . . . . . . . . . . . 16
         qTop 
          |
22 | 21 | ad3antrrr 736 |
. . . . . . . . . . . . . . 15
    
          qTop   
 
  qTop            |
23 | 18, 22 | mpbid 214 |
. . . . . . . . . . . . . 14
    
          qTop   
 
         |
24 | 23 | simprd 465 |
. . . . . . . . . . . . 13
    
          qTop   
 
       |
25 | | inss2 3653 |
. . . . . . . . . . . . . . . . 17
  qTop      |
26 | 25, 17 | sseldi 3430 |
. . . . . . . . . . . . . . . 16
    
          qTop   
 
   |
27 | 26 | elpwid 3961 |
. . . . . . . . . . . . . . 15
    
          qTop   
 
  |
28 | | imass2 5204 |
. . . . . . . . . . . . . . 15
             |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . 14
    
          qTop   
 
            |
30 | | elpwg 3959 |
. . . . . . . . . . . . . . 15
                               |
31 | 24, 30 | syl 17 |
. . . . . . . . . . . . . 14
    
          qTop   
 
                         |
32 | 29, 31 | mpbird 236 |
. . . . . . . . . . . . 13
    
          qTop   
 
             |
33 | 24, 32 | elind 3618 |
. . . . . . . . . . . 12
    
          qTop   
 
               |
34 | | simp-4r 777 |
. . . . . . . . . . . . . . 15
    
          qTop   
 
      |
35 | 34, 1 | syl 17 |
. . . . . . . . . . . . . 14
    
          qTop   
 
       |
36 | | f1ofn 5815 |
. . . . . . . . . . . . . 14
      
  |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . 13
    
          qTop   
 
   |
38 | 5 | ad2antrr 732 |
. . . . . . . . . . . . . 14
    
          qTop   
 
  |
39 | 27, 38 | sstrd 3442 |
. . . . . . . . . . . . 13
    
          qTop   
 
  |
40 | | simprr 766 |
. . . . . . . . . . . . 13
    
          qTop   
 
  |
41 | | fnfvima 6143 |
. . . . . . . . . . . . 13
  
             |
42 | 37, 39, 40, 41 | syl3anc 1268 |
. . . . . . . . . . . 12
    
          qTop   
 
            |
43 | | eleq2 2518 |
. . . . . . . . . . . . 13
                         |
44 | 43 | rspcev 3150 |
. . . . . . . . . . . 12
                          
                |
45 | 33, 42, 44 | syl2anc 667 |
. . . . . . . . . . 11
    
          qTop   
 
                 |
46 | 45 | rexlimdvaa 2880 |
. . . . . . . . . 10
        

  
  qTop
                      |
47 | | simp-4r 777 |
. . . . . . . . . . . . . . . . 17
    
                             |
48 | | f1ofun 5816 |
. . . . . . . . . . . . . . . . 17
    
  |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
    
                      
  |
50 | | inss2 3653 |
. . . . . . . . . . . . . . . . . 18
       
       |
51 | | simprl 764 |
. . . . . . . . . . . . . . . . . 18
    
                                 |
52 | 50, 51 | sseldi 3430 |
. . . . . . . . . . . . . . . . 17
    
                               |
53 | 52 | elpwid 3961 |
. . . . . . . . . . . . . . . 16
    
                              |
54 | | funimass2 5657 |
. . . . . . . . . . . . . . . 16
           
  |
55 | 49, 53, 54 | syl2anc 667 |
. . . . . . . . . . . . . . 15
    
                             |
56 | 5 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
    
                         |
57 | 55, 56 | sstrd 3442 |
. . . . . . . . . . . . . 14
    
                             |
58 | | f1of1 5813 |
. . . . . . . . . . . . . . . . 17
    
      |
59 | 47, 58 | syl 17 |
. . . . . . . . . . . . . . . 16
    
                             |
60 | | inss1 3652 |
. . . . . . . . . . . . . . . . . 18
       
 |
61 | 60, 51 | sseldi 3430 |
. . . . . . . . . . . . . . . . 17
    
                         |
62 | | elssuni 4227 |
. . . . . . . . . . . . . . . . . 18
    |
63 | 62, 19 | syl6sseqr 3479 |
. . . . . . . . . . . . . . . . 17
   |
64 | 61, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
    
                         |
65 | | f1imacnv 5830 |
. . . . . . . . . . . . . . . 16
     
            |
66 | 59, 64, 65 | syl2anc 667 |
. . . . . . . . . . . . . . 15
    
                                  |
67 | 66, 61 | eqeltrd 2529 |
. . . . . . . . . . . . . 14
    
                                  |
68 | 19 | elqtop2 20716 |
. . . . . . . . . . . . . . . 16
             qTop 
                  |
69 | 7, 68 | sylan2 477 |
. . . . . . . . . . . . . . 15
             qTop 
                  |
70 | 69 | ad3antrrr 736 |
. . . . . . . . . . . . . 14
    
                             qTop                    |
71 | 57, 67, 70 | mpbir2and 933 |
. . . . . . . . . . . . 13
    
                            qTop    |
72 | | vex 3048 |
. . . . . . . . . . . . . . 15
 |
73 | 72 | elpw2 4567 |
. . . . . . . . . . . . . 14
     
      |
74 | 55, 73 | sylibr 216 |
. . . . . . . . . . . . 13
    
                              |
75 | 71, 74 | elind 3618 |
. . . . . . . . . . . 12
    
                             qTop      |
76 | 5 | sselda 3432 |
. . . . . . . . . . . . . . 15
        

   |
77 | 76 | adantr 467 |
. . . . . . . . . . . . . 14
    
                         |
78 | | f1ocnvfv2 6176 |
. . . . . . . . . . . . . 14
     
            |
79 | 47, 77, 78 | syl2anc 667 |
. . . . . . . . . . . . 13
    
                                  |
80 | | f1ofn 5815 |
. . . . . . . . . . . . . . . 16
    
  |
81 | 80 | adantl 468 |
. . . . . . . . . . . . . . 15
         |
82 | 81 | ad3antrrr 736 |
. . . . . . . . . . . . . 14
    
                         |
83 | | simprr 766 |
. . . . . . . . . . . . . 14
    
                              |
84 | | fnfvima 6143 |
. . . . . . . . . . . . . 14
                       |
85 | 82, 64, 83, 84 | syl3anc 1268 |
. . . . . . . . . . . . 13
    
                                      |
86 | 79, 85 | eqeltrrd 2530 |
. . . . . . . . . . . 12
    
                             |
87 | | eleq2 2518 |
. . . . . . . . . . . . 13
     
       |
88 | 87 | rspcev 3150 |
. . . . . . . . . . . 12
        qTop   
     
  qTop
      |
89 | 75, 86, 88 | syl2anc 667 |
. . . . . . . . . . 11
    
                          qTop       |
90 | 89 | rexlimdvaa 2880 |
. . . . . . . . . 10
        

  
                 qTop        |
91 | 46, 90 | impbid 194 |
. . . . . . . . 9
        

  
  qTop
   
                  |
92 | | eluni2 4202 |
. . . . . . . . 9
    qTop   
   qTop 
     |
93 | | eluni2 4202 |
. . . . . . . . 9
                                |
94 | 91, 92, 93 | 3bitr4g 292 |
. . . . . . . 8
        

     qTop
  
                 |
95 | 94 | ralbidva 2824 |
. . . . . . 7
          
   qTop
  

                 |
96 | 15, 95 | syl5bb 261 |
. . . . . 6
         
   qTop
  

                 |
97 | 14, 96 | bitr4d 260 |
. . . . 5
                       
   qTop
      |
98 | | eltg 19972 |
. . . . . 6
                            |
99 | 98 | ad2antrr 732 |
. . . . 5
                  
                 |
100 | | ovex 6318 |
. . . . . 6
 qTop   |
101 | | eltg 19972 |
. . . . . 6
  qTop       qTop  
   qTop
      |
102 | 100, 101 | mp1i 13 |
. . . . 5
              qTop  
   qTop
      |
103 | 97, 99, 102 | 3bitr4d 289 |
. . . 4
                  
    qTop      |
104 | 103 | pm5.32da 647 |
. . 3
                   
    qTop       |
105 | | tgtopon 19987 |
. . . . . 6
     TopOn     |
106 | 105 | adantr 467 |
. . . . 5
           TopOn     |
107 | 19 | fveq2i 5868 |
. . . . 5
TopOn  TopOn    |
108 | 106, 107 | syl6eleqr 2540 |
. . . 4
           TopOn    |
109 | 7 | adantl 468 |
. . . 4
             |
110 | | elqtop3 20718 |
. . . 4
      TopOn      
      qTop 
              |
111 | 108, 109,
110 | syl2anc 667 |
. . 3
             qTop                |
112 | | unitg 19982 |
. . . . . . . . 9
  qTop       qTop     qTop    |
113 | 100, 112 | ax-mp 5 |
. . . . . . . 8
     qTop    
qTop   |
114 | 19 | elqtop2 20716 |
. . . . . . . . . . . 12
         qTop 
          |
115 | 7, 114 | sylan2 477 |
. . . . . . . . . . 11
         qTop 
          |
116 | | simpl 459 |
. . . . . . . . . . . 12
 
        |
117 | | selpw 3958 |
. . . . . . . . . . . 12
 
  |
118 | 116, 117 | sylibr 216 |
. . . . . . . . . . 11
 
     
   |
119 | 115, 118 | syl6bi 232 |
. . . . . . . . . 10
         qTop      |
120 | 119 | ssrdv 3438 |
. . . . . . . . 9
        qTop     |
121 | | sspwuni 4367 |
. . . . . . . . 9
  qTop  
  qTop 
  |
122 | 120, 121 | sylib 200 |
. . . . . . . 8
         qTop    |
123 | 113, 122 | syl5eqss 3476 |
. . . . . . 7
            qTop     |
124 | | sspwuni 4367 |
. . . . . . 7
     qTop         qTop     |
125 | 123, 124 | sylibr 216 |
. . . . . 6
           qTop      |
126 | 125 | sseld 3431 |
. . . . 5
            qTop  
    |
127 | 126, 117 | syl6ib 230 |
. . . 4
            qTop  
   |
128 | 127 | pm4.71rd 641 |
. . 3
            qTop        qTop       |
129 | 104, 111,
128 | 3bitr4d 289 |
. 2
             qTop 
    qTop      |
130 | 129 | eqrdv 2449 |
1
            qTop      qTop     |