Step | Hyp | Ref
| Expression |
1 | | eqid 2471 |
. . . 4
   |
2 | 1 | qtopres 20790 |
. . 3
  qTop   qTop       |
3 | 2 | 3ad2ant2 1052 |
. 2
 
  qTop   qTop       |
4 | | simp1 1030 |
. . . . . . . . . . . . 13
 
   |
5 | | funres 5628 |
. . . . . . . . . . . . . . 15

     |
6 | 5 | 3ad2ant3 1053 |
. . . . . . . . . . . . . 14
 
 
    |
7 | | funforn 5813 |
. . . . . . . . . . . . . 14
         
         |
8 | 6, 7 | sylib 201 |
. . . . . . . . . . . . 13
 
                |
9 | | dmres 5131 |
. . . . . . . . . . . . . . 15
       |
10 | | inss1 3643 |
. . . . . . . . . . . . . . 15
 
   |
11 | 9, 10 | eqsstri 3448 |
. . . . . . . . . . . . . 14
     |
12 | 11 | a1i 11 |
. . . . . . . . . . . . 13
 
 
 
   |
13 | 1 | elqtop 20789 |
. . . . . . . . . . . . 13
  
            
 
    qTop      
 
  
         |
14 | 4, 8, 12, 13 | syl3anc 1292 |
. . . . . . . . . . . 12
 
   qTop    
                |
15 | 14 | simprbda 635 |
. . . . . . . . . . 11
     qTop     
     |
16 | | selpw 3949 |
. . . . . . . . . . 11
    
     |
17 | 15, 16 | sylibr 217 |
. . . . . . . . . 10
     qTop     
      |
18 | 17 | ex 441 |
. . . . . . . . 9
 
   qTop            |
19 | 18 | ssrdv 3424 |
. . . . . . . 8
 
  qTop           |
20 | | sstr2 3425 |
. . . . . . . 8
  qTop    
  qTop        
       |
21 | 19, 20 | syl5com 30 |
. . . . . . 7
 
 
 qTop 
   
      |
22 | | sspwuni 4360 |
. . . . . . 7
    
      |
23 | 21, 22 | syl6ib 234 |
. . . . . 6
 
 
 qTop 
          |
24 | | imauni 6169 |
. . . . . . . 8
         
  
      |
25 | | simpl1 1033 |
. . . . . . . . 9
     qTop     
  |
26 | 14 | simplbda 636 |
. . . . . . . . . . 11
     qTop     
  
       |
27 | 26 | ralrimiva 2809 |
. . . . . . . . . 10
 
   qTop                |
28 | | ssralv 3479 |
. . . . . . . . . 10
  qTop    
 
 qTop 
            
  
        |
29 | 27, 28 | mpan9 477 |
. . . . . . . . 9
     qTop     

  
       |
30 | | iunopn 20005 |
. . . . . . . . 9
                       |
31 | 25, 29, 30 | syl2anc 673 |
. . . . . . . 8
     qTop     
   
       |
32 | 24, 31 | syl5eqel 2553 |
. . . . . . 7
     qTop     
  
        |
33 | 32 | ex 441 |
. . . . . 6
 
 
 qTop 
               |
34 | 23, 33 | jcad 542 |
. . . . 5
 
 
 qTop 
    
     
          |
35 | 1 | elqtop 20789 |
. . . . . 6
  
            
 
     qTop         
  
          |
36 | 4, 8, 12, 35 | syl3anc 1292 |
. . . . 5
 
  
 qTop    
                  |
37 | 34, 36 | sylibrd 242 |
. . . 4
 
 
 qTop 
     qTop        |
38 | 37 | alrimiv 1781 |
. . 3
 
     qTop       qTop        |
39 | | inss1 3643 |
. . . . . 6
   |
40 | 1 | elqtop 20789 |
. . . . . . . . . 10
  
            
 
    qTop      
 
  
         |
41 | 4, 8, 12, 40 | syl3anc 1292 |
. . . . . . . . 9
 
   qTop    
                |
42 | 41 | biimpa 492 |
. . . . . . . 8
     qTop     
               |
43 | 42 | adantrr 731 |
. . . . . . 7
      qTop      qTop       
              |
44 | 43 | simpld 466 |
. . . . . 6
      qTop      qTop            |
45 | 39, 44 | syl5ss 3429 |
. . . . 5
      qTop      qTop       
      |
46 | 6 | adantr 472 |
. . . . . . 7
      qTop      qTop       
    |
47 | | inpreima 6022 |
. . . . . . 7
   
  
                  
        |
48 | 46, 47 | syl 17 |
. . . . . 6
      qTop      qTop              
          
  
        |
49 | 4 | adantr 472 |
. . . . . . 7
      qTop      qTop         |
50 | 43 | simprd 470 |
. . . . . . 7
      qTop      qTop                 |
51 | 26 | adantrl 730 |
. . . . . . 7
      qTop      qTop                 |
52 | | inopn 20006 |
. . . . . . 7
                              
        |
53 | 49, 50, 51, 52 | syl3anc 1292 |
. . . . . 6
      qTop      qTop                           |
54 | 48, 53 | eqeltrd 2549 |
. . . . 5
      qTop      qTop              
    |
55 | 1 | elqtop 20789 |
. . . . . . 7
  
            
 
      qTop        
 
  
           |
56 | 4, 8, 12, 55 | syl3anc 1292 |
. . . . . 6
 
     qTop    
 
           
      |
57 | 56 | adantr 472 |
. . . . 5
      qTop      qTop           qTop    
 
           
      |
58 | 45, 54, 57 | mpbir2and 936 |
. . . 4
      qTop      qTop       
  qTop       |
59 | 58 | ralrimivva 2814 |
. . 3
 
   qTop        qTop         qTop       |
60 | | ovex 6336 |
. . . 4
 qTop      |
61 | | istopg 20002 |
. . . 4
  qTop       qTop         
qTop       qTop        qTop        qTop         qTop         |
62 | 60, 61 | ax-mp 5 |
. . 3
  qTop        
 qTop 
     qTop        qTop        qTop         qTop        |
63 | 38, 59, 62 | sylanbrc 677 |
. 2
 
  qTop       |
64 | 3, 63 | eqeltrd 2549 |
1
 
  qTop    |