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

        |
4 | 3 | adantr 472 |
. . 3
  UHGraph
      NeighbVtx 
 

   
    |
5 | 2 | eleq2i 2541 |
. . . . . . . . . 10

Edg    |
6 | | edguhgr 39382 |
. . . . . . . . . 10
  UHGraph
Edg  
 Vtx    |
7 | 5, 6 | sylan2b 483 |
. . . . . . . . 9
  UHGraph
  Vtx    |
8 | 1 | eqeq1i 2476 |
. . . . . . . . . . . . 13
   
Vtx       |
9 | | pweq 3945 |
. . . . . . . . . . . . . . 15
 Vtx    
 Vtx        |
10 | 9 | eleq2d 2534 |
. . . . . . . . . . . . . 14
 Vtx    
  Vtx         |
11 | | selpw 3949 |
. . . . . . . . . . . . . 14
    
     |
12 | 10, 11 | syl6bb 269 |
. . . . . . . . . . . . 13
 Vtx    
  Vtx        |
13 | 8, 12 | sylbi 200 |
. . . . . . . . . . . 12
      Vtx 
      |
14 | 13 | adantl 473 |
. . . . . . . . . . 11
   UHGraph        Vtx 
      |
15 | | prcom 4041 |
. . . . . . . . . . . . . . . 16
       |
16 | 15 | sseq1i 3442 |
. . . . . . . . . . . . . . 15
   
     |
17 | | eqss 3433 |
. . . . . . . . . . . . . . . . 17
   
          |
18 | | eleq1a 2544 |
. . . . . . . . . . . . . . . . . . 19
           |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
  

             |
20 | 19 | com13 82 |
. . . . . . . . . . . . . . . . 17
                 |
21 | 17, 20 | sylbir 218 |
. . . . . . . . . . . . . . . 16
    
                 |
22 | 21 | ex 441 |
. . . . . . . . . . . . . . 15
    
                 |
23 | 16, 22 | sylbi 200 |
. . . . . . . . . . . . . 14
    
                 |
24 | 23 | com13 82 |
. . . . . . . . . . . . 13
 
      
             |
25 | 24 | adantl 473 |
. . . . . . . . . . . 12
  UHGraph
 
      
             |
26 | 25 | adantr 472 |
. . . . . . . . . . 11
   UHGraph      
      
             |
27 | 14, 26 | sylbid 223 |
. . . . . . . . . 10
   UHGraph        Vtx     
             |
28 | 27 | ex 441 |
. . . . . . . . 9
  UHGraph
 
     Vtx     
              |
29 | 7, 28 | mpid 41 |
. . . . . . . 8
  UHGraph
 
      
             |
30 | 29 | impancom 447 |
. . . . . . 7
  UHGraph
                      |
31 | 30 | com14 90 |
. . . . . 6
  

        UHGraph
   
        |
32 | 31 | rexlimdv 2870 |
. . . . 5
  

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

    
 
UHGraph           |
34 | 33 | com12 31 |
. . 3
  UHGraph
       

          |
35 | 4, 34 | sylbid 223 |
. 2
  UHGraph
      NeighbVtx        |
36 | 35 | 3impia 1228 |
1
  UHGraph
    NeighbVtx
 
     |