Step | Hyp | Ref
| Expression |
1 | | cusisusgra 25242 |
. . 3
 ComplUSGrph USGrph
  |
2 | | nbusgra 25212 |
. . . . . . 7
 USGrph     Neighbors         |
3 | 2 | adantr 471 |
. . . . . 6
  USGrph
ComplUSGrph      Neighbors         |
4 | 3 | adantr 471 |
. . . . 5
   USGrph ComplUSGrph       Neighbors  
 
    |
5 | | usgrav 25121 |
. . . . . . . . . 10
 USGrph 
   |
6 | | iscusgra 25240 |
. . . . . . . . . 10
 
  ComplUSGrph
 USGrph               |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
 USGrph  ComplUSGrph
 USGrph               |
8 | 7 | biimpa 491 |
. . . . . . . 8
  USGrph
ComplUSGrph   USGrph  
           |
9 | | df-ral 2754 |
. . . . . . . . . 10
 

       
               |
10 | | preq2 4065 |
. . . . . . . . . . . . . . 15
     
   |
11 | 10 | eleq1d 2524 |
. . . . . . . . . . . . . 14
    
      |
12 | 11 | elrab 3208 |
. . . . . . . . . . . . 13
             |
13 | | pm2.24 113 |
. . . . . . . . . . . . . . . . . . 19
 
       |
14 | 13 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
      

      |
15 | 14 | com12 32 |
. . . . . . . . . . . . . . . . 17
      

      |
16 | | eldif 3426 |
. . . . . . . . . . . . . . . . . . 19
    

     |
17 | | pm2.24 113 |
. . . . . . . . . . . . . . . . . . . 20
 
   
    |
18 | 17 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
 
   
   
    |
19 | 16, 18 | sylbi 200 |
. . . . . . . . . . . . . . . . . 18
     

       |
20 | 19 | com12 32 |
. . . . . . . . . . . . . . . . 17
              |
21 | 15, 20 | impbid 195 |
. . . . . . . . . . . . . . . 16
      
       |
22 | 21 | a1d 26 |
. . . . . . . . . . . . . . 15
   USGrph

     

       |
23 | | usgraedgrn 25164 |
. . . . . . . . . . . . . . . . . . . . . . 23
  USGrph
   
  |
24 | | elsni 4005 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
25 | | eqcom 2469 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  |
26 | 24, 25 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
27 | 26 | necon3ai 2661 |
. . . . . . . . . . . . . . . . . . . . . . 23

    |
28 | 23, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
  USGrph
   
    |
29 | 28 | ex 440 |
. . . . . . . . . . . . . . . . . . . . 21
 USGrph    
     |
30 | 29 | ad2antrl 739 |
. . . . . . . . . . . . . . . . . . . 20
            USGrph      
     |
31 | 30 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
             USGrph  
    
     |
32 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
   |
33 | | elsncg 4003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
     |
34 | | elsn 3994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
35 | 34 | biimpri 211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     |
36 | 25, 35 | sylbi 200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     |
37 | 33, 36 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
       |
38 | 37 | con3d 140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
 
     |
39 | 38 | impcom 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   

    |
40 | 32, 39 | eldifd 3427 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
       |
41 | | preq1 4064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         |
42 | 41 | eleq1d 2524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
      |
43 | 42 | rspcva 3160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
               |
44 | 43 | 2a1d 27 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
            USGrph        |
45 | 44 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 USGrph
        |
46 | 45 | com24 90 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      USGrph                    |
47 | 40, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
  USGrph

 
       
        |
48 | 47 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
 USGrph 
 
       
         |
49 | 48 | com13 83 |
. . . . . . . . . . . . . . . . . . . . . . 23
 USGrph 

  
 
       
         |
50 | 49 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . 22
  USGrph
 
  
 
       
        |
51 | 50 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
     USGrph 

 
       
        |
52 | 51 | com14 91 |
. . . . . . . . . . . . . . . . . . . 20
 
       
  USGrph


     
     |
53 | 52 | imp31 438 |
. . . . . . . . . . . . . . . . . . 19
             USGrph  
          |
54 | 31, 53 | impbid 195 |
. . . . . . . . . . . . . . . . . 18
             USGrph  
    
     |
55 | 54 | pm5.32da 651 |
. . . . . . . . . . . . . . . . 17
            USGrph       
        |
56 | 55, 16 | syl6bbr 271 |
. . . . . . . . . . . . . . . 16
            USGrph       
        |
57 | 56 | ex 440 |
. . . . . . . . . . . . . . 15
 
       
  USGrph

     

       |
58 | 22, 57 | ja 166 |
. . . . . . . . . . . . . 14
  
        
  USGrph      
         |
59 | 58 | impcom 436 |
. . . . . . . . . . . . 13
   USGrph
                  
       |
60 | 12, 59 | syl5bb 265 |
. . . . . . . . . . . 12
   USGrph
                  

      |
61 | 60 | ex 440 |
. . . . . . . . . . 11
  USGrph
              
 
 

       |
62 | 61 | alimdv 1774 |
. . . . . . . . . 10
  USGrph
    
                
         |
63 | 9, 62 | syl5bi 225 |
. . . . . . . . 9
  USGrph
  

               
        |
64 | 63 | impancom 446 |
. . . . . . . 8
  USGrph

                  
        |
65 | 8, 64 | syl 17 |
. . . . . . 7
  USGrph
ComplUSGrph  
       

       |
66 | 65 | imp 435 |
. . . . . 6
   USGrph ComplUSGrph          

      |
67 | | dfcleq 2456 |
. . . . . 6
      
  
       

      |
68 | 66, 67 | sylibr 217 |
. . . . 5
   USGrph ComplUSGrph   
 
  
     |
69 | 4, 68 | eqtrd 2496 |
. . . 4
   USGrph ComplUSGrph       Neighbors        |
70 | 69 | ex 440 |
. . 3
  USGrph
ComplUSGrph  
    Neighbors         |
71 | 1, 70 | mpancom 680 |
. 2
 ComplUSGrph 
    Neighbors         |
72 | 71 | imp 435 |
1
  ComplUSGrph      Neighbors        |