Step | Hyp | Ref
| Expression |
1 | | simp1 957 |
. 2
              |
2 | | smprngpr.1 |
. . . . 5
     |
3 | | smprngpr.4 |
. . . . 5
GId   |
4 | 2, 3 | 0idl 26533 |
. . . 4
         |
5 | 4 | 3ad2ant1 978 |
. . 3
             
      |
6 | | smprngpr.2 |
. . . . . . . 8
     |
7 | | smprngpr.3 |
. . . . . . . 8
 |
8 | | smprngpr.5 |
. . . . . . . 8
GId   |
9 | 2, 6, 7, 3, 8 | 0rngo 26535 |
. . . . . . 7
 
     |
10 | | eqcom 2414 |
. . . . . . 7

  |
11 | | eqcom 2414 |
. . . . . . 7
       |
12 | 9, 10, 11 | 3bitr4g 280 |
. . . . . 6
       |
13 | 12 | necon3bid 2610 |
. . . . 5
       |
14 | 13 | biimpa 471 |
. . . 4
       |
15 | 14 | 3adant3 977 |
. . 3
                |
16 | | df-pr 3789 |
. . . . . . . 8
              |
17 | 16 | eqeq2i 2422 |
. . . . . . 7
        
               |
18 | | eleq2 2473 |
. . . . . . . . 9
                 
    
      |
19 | | eleq2 2473 |
. . . . . . . . 9
                 
    
      |
20 | 18, 19 | anbi12d 692 |
. . . . . . . 8
                             
       
       |
21 | | elun 3456 |
. . . . . . . . . 10
        
    
     |
22 | | elsn 3797 |
. . . . . . . . . . 11
    
    |
23 | | elsn 3797 |
. . . . . . . . . . 11
     |
24 | 22, 23 | orbi12i 508 |
. . . . . . . . . 10
           
   |
25 | 21, 24 | bitri 241 |
. . . . . . . . 9
        
  
   |
26 | | elun 3456 |
. . . . . . . . . 10
        
    
     |
27 | | elsn 3797 |
. . . . . . . . . . 11
    
    |
28 | | elsn 3797 |
. . . . . . . . . . 11
     |
29 | 27, 28 | orbi12i 508 |
. . . . . . . . . 10
           
   |
30 | 26, 29 | bitri 241 |
. . . . . . . . 9
        
  
   |
31 | 25, 30 | anbi12i 679 |
. . . . . . . 8
              
   
   
   
    |
32 | 20, 31 | syl6bb 253 |
. . . . . . 7
                           

  
     |
33 | 17, 32 | sylbi 188 |
. . . . . 6
        
      
        

  
     |
34 | 33 | 3ad2ant3 980 |
. . . . 5
                          

  
     |
35 | | eqimss 3368 |
. . . . . . . . . . 11
  
    |
36 | 35 | orcd 382 |
. . . . . . . . . 10
     
     |
37 | 36 | adantr 452 |
. . . . . . . . 9
       
 
     |
38 | 37 | a1d 23 |
. . . . . . . 8
        

               |
39 | 38 | a1i 11 |
. . . . . . 7
      
    

      
 
       |
40 | | eqimss 3368 |
. . . . . . . . . . 11
  
    |
41 | 40 | olcd 383 |
. . . . . . . . . 10
     
     |
42 | 41 | adantl 453 |
. . . . . . . . 9
 
   
 
     |
43 | 42 | a1d 23 |
. . . . . . . 8
 
    

               |
44 | 43 | a1i 11 |
. . . . . . 7
         

                |
45 | 36 | adantr 452 |
. . . . . . . . 9
    
        |
46 | 45 | a1d 23 |
. . . . . . . 8
    
 

        
      |
47 | 46 | a1i 11 |
. . . . . . 7
      
  

                |
48 | 2 | rneqi 5063 |
. . . . . . . . . . . . . 14
     |
49 | 7, 48 | eqtri 2432 |
. . . . . . . . . . . . 13
     |
50 | 49, 6, 8 | rngo1cl 21978 |
. . . . . . . . . . . 12
   |
51 | 50 | adantr 452 |
. . . . . . . . . . 11
     |
52 | 6, 49, 8 | rngolidm 21973 |
. . . . . . . . . . . . . . . 16
         |
53 | 50, 52 | mpdan 650 |
. . . . . . . . . . . . . . 15
       |
54 | 53 | eleq1d 2478 |
. . . . . . . . . . . . . 14
       
     |
55 | | fvex 5709 |
. . . . . . . . . . . . . . . 16
GId   |
56 | 8, 55 | eqeltri 2482 |
. . . . . . . . . . . . . . 15
 |
57 | 56 | elsnc 3805 |
. . . . . . . . . . . . . 14
     |
58 | 54, 57 | syl6bb 253 |
. . . . . . . . . . . . 13
       
   |
59 | 58 | necon3bbid 2609 |
. . . . . . . . . . . 12
       
   |
60 | 59 | biimpar 472 |
. . . . . . . . . . 11
           |
61 | | oveq1 6055 |
. . . . . . . . . . . . . 14
           |
62 | 61 | eleq1d 2478 |
. . . . . . . . . . . . 13
                 |
63 | 62 | notbid 286 |
. . . . . . . . . . . 12
                 |
64 | | oveq2 6056 |
. . . . . . . . . . . . . 14
           |
65 | 64 | eleq1d 2478 |
. . . . . . . . . . . . 13
                 |
66 | 65 | notbid 286 |
. . . . . . . . . . . 12
                 |
67 | 63, 66 | rspc2ev 3028 |
. . . . . . . . . . 11
 
       

        |
68 | 51, 51, 60, 67 | syl3anc 1184 |
. . . . . . . . . 10
   

        |
69 | | rexnal 2685 |
. . . . . . . . . . . 12
                 |
70 | 69 | rexbii 2699 |
. . . . . . . . . . 11
  
                |
71 | | rexnal 2685 |
. . . . . . . . . . 11
          
        |
72 | 70, 71 | bitri 241 |
. . . . . . . . . 10
  
                |
73 | 68, 72 | sylib 189 |
. . . . . . . . 9
    
        |
74 | 73 | pm2.21d 100 |
. . . . . . . 8
    

               |
75 | | raleq 2872 |
. . . . . . . . . 10
  

       
         |
76 | | raleq 2872 |
. . . . . . . . . . 11
  
                |
77 | 76 | ralbidv 2694 |
. . . . . . . . . 10
  

       
         |
78 | 75, 77 | sylan9bb 681 |
. . . . . . . . 9
 
         
 
         |
79 | 78 | imbi1d 309 |
. . . . . . . 8
 
   

      
 
            
  
       |
80 | 74, 79 | syl5ibrcom 214 |
. . . . . . 7
     
 

        
       |
81 | 39, 44, 47, 80 | ccased 914 |
. . . . . 6
       
   
          
  
       |
82 | 81 | 3adant3 977 |
. . . . 5
                
   
          
  
       |
83 | 34, 82 | sylbid 207 |
. . . 4
                      
 

        
       |
84 | 83 | ralrimivv 2765 |
. . 3
                         

      
 
      |
85 | 2, 6, 7 | ispridl 26542 |
. . . 4
   
   
  
                          
  
        |
86 | 85 | 3ad2ant1 978 |
. . 3
                  
  
                          
  
        |
87 | 5, 15, 84, 86 | mpbir3and 1137 |
. 2
             
      |
88 | 2, 3 | isprrngo 26558 |
. 2
           |
89 | 1, 87, 88 | sylanbrc 646 |
1
              |