Step | Hyp | Ref
| Expression |
1 | | nbgr2vtx1edg.v |
. . . . 5
Vtx   |
2 | | nbgr2vtx1edg.e |
. . . . 5
Edg   |
3 | 1, 2 | nbgrel 39410 |
. . . 4
 UHGraph   NeighbVtx
  

        |
4 | 3 | adantr 467 |
. . 3
  UHGraph
      NeighbVtx 
 

   
    |
5 | 2 | eleq2i 2521 |
. . . . . . . . . 10

Edg    |
6 | | edguhgr 39221 |
. . . . . . . . . 10
  UHGraph
Edg  
 Vtx    |
7 | 5, 6 | sylan2b 478 |
. . . . . . . . 9
  UHGraph
  Vtx    |
8 | 1 | eqeq1i 2456 |
. . . . . . . . . . . . 13
   
Vtx       |
9 | | pweq 3954 |
. . . . . . . . . . . . . . 15
 Vtx    
 Vtx        |
10 | 9 | eleq2d 2514 |
. . . . . . . . . . . . . 14
 Vtx    
  Vtx         |
11 | | selpw 3958 |
. . . . . . . . . . . . . 14
    
     |
12 | 10, 11 | syl6bb 265 |
. . . . . . . . . . . . 13
 Vtx    
  Vtx        |
13 | 8, 12 | sylbi 199 |
. . . . . . . . . . . 12
      Vtx 
      |
14 | 13 | adantl 468 |
. . . . . . . . . . 11
   UHGraph        Vtx 
      |
15 | | prcom 4050 |
. . . . . . . . . . . . . . . 16
       |
16 | 15 | sseq1i 3456 |
. . . . . . . . . . . . . . 15
   
     |
17 | | eqss 3447 |
. . . . . . . . . . . . . . . . 17
   
          |
18 | | eleq1a 2524 |
. . . . . . . . . . . . . . . . . . 19
           |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
  

             |
20 | 19 | com13 83 |
. . . . . . . . . . . . . . . . 17
                 |
21 | 17, 20 | sylbir 217 |
. . . . . . . . . . . . . . . 16
    
                 |
22 | 21 | ex 436 |
. . . . . . . . . . . . . . 15
    
                 |
23 | 16, 22 | sylbi 199 |
. . . . . . . . . . . . . 14
    
                 |
24 | 23 | com13 83 |
. . . . . . . . . . . . 13
 
      
             |
25 | 24 | adantl 468 |
. . . . . . . . . . . 12
  UHGraph
 
      
             |
26 | 25 | adantr 467 |
. . . . . . . . . . 11
   UHGraph      
      
             |
27 | 14, 26 | sylbid 219 |
. . . . . . . . . 10
   UHGraph        Vtx     
             |
28 | 27 | ex 436 |
. . . . . . . . 9
  UHGraph
 
     Vtx     
              |
29 | 7, 28 | mpid 42 |
. . . . . . . 8
  UHGraph
 
      
             |
30 | 29 | impancom 442 |
. . . . . . 7
  UHGraph
                      |
31 | 30 | com14 91 |
. . . . . 6
  

        UHGraph
   
        |
32 | 31 | rexlimdv 2877 |
. . . . 5
  

  
  
  UHGraph            |
33 | 32 | 3impia 1205 |
. . . 4
  

    
 
UHGraph           |
34 | 33 | com12 32 |
. . 3
  UHGraph
       

          |
35 | 4, 34 | sylbid 219 |
. 2
  UHGraph
      NeighbVtx        |
36 | 35 | 3impia 1205 |
1
  UHGraph
    NeighbVtx
 
     |