Step | Hyp | Ref
| Expression |
1 | | nbgr2vtx1edg.v |
. . . . 5
Vtx   |
2 | | fvex 5875 |
. . . . 5
Vtx   |
3 | 1, 2 | eqeltri 2525 |
. . . 4
 |
4 | | hash2prb 12633 |
. . . 4
     



       |
5 | 3, 4 | ax-mp 5 |
. . 3
    



      |
6 | | simpr 463 |
. . . . . . . . . . 11
  
  
   |
7 | 6 | ancomd 453 |
. . . . . . . . . 10
  
  
   |
8 | 7 | ad2antrr 732 |
. . . . . . . . 9
       
         
   |
9 | | simpl 459 |
. . . . . . . . . . 11
 
      |
10 | 9 | necomd 2679 |
. . . . . . . . . 10
 
      |
11 | 10 | ad2antlr 733 |
. . . . . . . . 9
       
           |
12 | | id 22 |
. . . . . . . . . . 11
         |
13 | | sseq2 3454 |
. . . . . . . . . . . 12
       
         |
14 | 13 | adantl 468 |
. . . . . . . . . . 11
    
          
      |
15 | | ssid 3451 |
. . . . . . . . . . . 12
       |
16 | 15 | a1i 11 |
. . . . . . . . . . 11
            |
17 | 12, 14, 16 | rspcedvd 3155 |
. . . . . . . . . 10
    
     |
18 | 17 | adantl 468 |
. . . . . . . . 9
       
         
  
  |
19 | | nbgr2vtx1edg.e |
. . . . . . . . . . 11
Edg   |
20 | 1, 19 | nbgrel 39410 |
. . . . . . . . . 10
   NeighbVtx 
 

   
    |
21 | 20 | ad3antrrr 736 |
. . . . . . . . 9
       
           NeighbVtx 
 

   
    |
22 | 8, 11, 18, 21 | mpbir3and 1191 |
. . . . . . . 8
       
          NeighbVtx    |
23 | 6 | ad2antrr 732 |
. . . . . . . . 9
       
         
   |
24 | 9 | ad2antlr 733 |
. . . . . . . . 9
       
           |
25 | | sseq2 3454 |
. . . . . . . . . . . 12
       
         |
26 | 25 | adantl 468 |
. . . . . . . . . . 11
    
          
      |
27 | | prcom 4050 |
. . . . . . . . . . . . 13
       |
28 | 27 | eqimssi 3486 |
. . . . . . . . . . . 12
       |
29 | 28 | a1i 11 |
. . . . . . . . . . 11
            |
30 | 12, 26, 29 | rspcedvd 3155 |
. . . . . . . . . 10
    
     |
31 | 30 | adantl 468 |
. . . . . . . . 9
       
         
  
  |
32 | 1, 19 | nbgrel 39410 |
. . . . . . . . . 10
   NeighbVtx 
 

   
    |
33 | 32 | ad3antrrr 736 |
. . . . . . . . 9
       
           NeighbVtx 
 

   
    |
34 | 23, 24, 31, 33 | mpbir3and 1191 |
. . . . . . . 8
       
          NeighbVtx    |
35 | | difprsn1 4108 |
. . . . . . . . . . . . 13
            |
36 | 35 | raleqdv 2993 |
. . . . . . . . . . . 12
  
         NeighbVtx
      NeighbVtx     |
37 | | vex 3048 |
. . . . . . . . . . . . 13
 |
38 | | eleq1 2517 |
. . . . . . . . . . . . 13
   NeighbVtx 

NeighbVtx     |
39 | 37, 38 | ralsn 4010 |
. . . . . . . . . . . 12
 
  
 NeighbVtx 

NeighbVtx    |
40 | 36, 39 | syl6bb 265 |
. . . . . . . . . . 11
  
         NeighbVtx
  NeighbVtx     |
41 | | difprsn2 4109 |
. . . . . . . . . . . . 13
            |
42 | 41 | raleqdv 2993 |
. . . . . . . . . . . 12
  
         NeighbVtx
      NeighbVtx     |
43 | | vex 3048 |
. . . . . . . . . . . . 13
 |
44 | | eleq1 2517 |
. . . . . . . . . . . . 13
   NeighbVtx 

NeighbVtx     |
45 | 43, 44 | ralsn 4010 |
. . . . . . . . . . . 12
 
  
 NeighbVtx 

NeighbVtx    |
46 | 42, 45 | syl6bb 265 |
. . . . . . . . . . 11
  
         NeighbVtx
  NeighbVtx     |
47 | 40, 46 | anbi12d 717 |
. . . . . . . . . 10
             NeighbVtx            NeighbVtx     NeighbVtx

 NeighbVtx      |
48 | 47 | adantr 467 |
. . . . . . . . 9
 
      
         NeighbVtx  
         NeighbVtx  
  NeighbVtx

 NeighbVtx      |
49 | 48 | ad2antlr 733 |
. . . . . . . 8
       
                     NeighbVtx            NeighbVtx     NeighbVtx

 NeighbVtx      |
50 | 22, 34, 49 | mpbir2and 933 |
. . . . . . 7
       
                    NeighbVtx            NeighbVtx     |
51 | 50 | ex 436 |
. . . . . 6
   
  
    
     
         NeighbVtx
           NeighbVtx
     |
52 | | eleq1 2517 |
. . . . . . . . 9
    
      |
53 | | id 22 |
. . . . . . . . . . 11
         |
54 | | difeq1 3544 |
. . . . . . . . . . . 12
                 |
55 | 54 | raleqdv 2993 |
. . . . . . . . . . 11
     
      NeighbVtx 
          NeighbVtx     |
56 | 53, 55 | raleqbidv 3001 |
. . . . . . . . . 10
     

      NeighbVtx 
               NeighbVtx     |
57 | | sneq 3978 |
. . . . . . . . . . . . . 14
       |
58 | 57 | difeq2d 3551 |
. . . . . . . . . . . . 13
                 |
59 | | oveq2 6298 |
. . . . . . . . . . . . . 14
  NeighbVtx   NeighbVtx    |
60 | 59 | eleq2d 2514 |
. . . . . . . . . . . . 13
   NeighbVtx 

NeighbVtx     |
61 | 58, 60 | raleqbidv 3001 |
. . . . . . . . . . . 12
  
         NeighbVtx
           NeighbVtx     |
62 | 61 | idi 2 |
. . . . . . . . . . 11
  
         NeighbVtx
           NeighbVtx     |
63 | | sneq 3978 |
. . . . . . . . . . . . 13
       |
64 | 63 | difeq2d 3551 |
. . . . . . . . . . . 12
                 |
65 | | oveq2 6298 |
. . . . . . . . . . . . 13
  NeighbVtx   NeighbVtx    |
66 | 65 | eleq2d 2514 |
. . . . . . . . . . . 12
   NeighbVtx 

NeighbVtx     |
67 | 64, 66 | raleqbidv 3001 |
. . . . . . . . . . 11
  
         NeighbVtx
           NeighbVtx     |
68 | 43, 37, 62, 67 | ralpr 4025 |
. . . . . . . . . 10
 
    
         NeighbVtx 
 
         NeighbVtx  
         NeighbVtx     |
69 | 56, 68 | syl6bb 265 |
. . . . . . . . 9
     

      NeighbVtx 
 
         NeighbVtx  
         NeighbVtx      |
70 | 52, 69 | imbi12d 322 |
. . . . . . . 8
       
      NeighbVtx  
     
         NeighbVtx
           NeighbVtx
      |
71 | 70 | adantl 468 |
. . . . . . 7
 
      
       NeighbVtx                  NeighbVtx            NeighbVtx       |
72 | 71 | adantl 468 |
. . . . . 6
   
  
    
 
 
      NeighbVtx  
     
         NeighbVtx
           NeighbVtx
      |
73 | 51, 72 | mpbird 236 |
. . . . 5
   
  
    


       NeighbVtx     |
74 | 73 | ex 436 |
. . . 4
  
   
   


       NeighbVtx      |
75 | 74 | rexlimdvva 2886 |
. . 3
  


   


       NeighbVtx      |
76 | 5, 75 | syl5bi 221 |
. 2
      
 
      NeighbVtx      |
77 | 76 | 3imp 1202 |
1
       
       NeighbVtx    |