Step | Hyp | Ref
| Expression |
1 | | frgrancvvdeq.ny |
. . 3
    Neighbors   |
2 | 1 | ineq2i 3622 |
. 2
     Neighbors 
    
 Neighbors 
    Neighbors    |
3 | | frgrancvvdeq.nx |
. . . . . . 7
    Neighbors   |
4 | 3 | eleq2i 2541 |
. . . . . 6

    Neighbors    |
5 | | frgrancvvdeq.f |
. . . . . . . 8
 FriendGrph   |
6 | | frisusgra 25799 |
. . . . . . . 8
 FriendGrph USGrph
  |
7 | 5, 6 | syl 17 |
. . . . . . 7
 USGrph   |
8 | | nbgraisvtx 25238 |
. . . . . . 7
 USGrph      Neighbors     |
9 | 7, 8 | syl 17 |
. . . . . 6
      Neighbors 
   |
10 | 4, 9 | syl5bi 225 |
. . . . 5
     |
11 | 10 | imp 436 |
. . . 4
 
   |
12 | | frgrancvvdeq.x |
. . . . 5
   |
13 | | frgrancvvdeq.y |
. . . . 5
   |
14 | | frgrancvvdeq.ne |
. . . . 5
   |
15 | | frgrancvvdeq.xy |
. . . . 5
   |
16 | | frgrancvvdeq.a |
. . . . 5
         |
17 | 3, 1, 12, 13, 14, 15, 5, 16 | frgrancvvdeqlem1 25837 |
. . . 4
 
       |
18 | 5 | adantr 472 |
. . . . 5
 
 FriendGrph   |
19 | | frisusgranb 25804 |
. . . . 5
 FriendGrph  
         
 Neighbors 
    Neighbors       |
20 | 18, 19 | syl 17 |
. . . 4
 
 
            Neighbors      Neighbors       |
21 | 11, 17, 20 | jca31 543 |
. . 3
 
  
     

           Neighbors      Neighbors        |
22 | | sneq 3969 |
. . . . . . . . 9
       |
23 | 22 | difeq2d 3540 |
. . . . . . . 8
           |
24 | | oveq2 6316 |
. . . . . . . . . . 11
     Neighbors    
 Neighbors    |
25 | 24 | ineq1d 3624 |
. . . . . . . . . 10
      Neighbors      Neighbors        Neighbors      Neighbors     |
26 | 25 | eqeq1d 2473 |
. . . . . . . . 9
       Neighbors      Neighbors    
     Neighbors 
    Neighbors        |
27 | 26 | rexbidv 2892 |
. . . . . . . 8
  
     Neighbors      Neighbors    

     Neighbors 
    Neighbors        |
28 | 23, 27 | raleqbidv 2987 |
. . . . . . 7
  
         
 Neighbors 
    Neighbors           
     Neighbors 
    Neighbors        |
29 | 28 | rspcva 3134 |
. . . . . 6
   
           Neighbors      Neighbors      
         
 Neighbors 
    Neighbors       |
30 | | oveq2 6316 |
. . . . . . . . . . . 12
     Neighbors    
 Neighbors    |
31 | 30 | ineq2d 3625 |
. . . . . . . . . . 11
      Neighbors      Neighbors        Neighbors      Neighbors     |
32 | 31 | eqeq1d 2473 |
. . . . . . . . . 10
       Neighbors      Neighbors    
     Neighbors 
    Neighbors        |
33 | 32 | rexbidv 2892 |
. . . . . . . . 9
  
     Neighbors      Neighbors    

     Neighbors 
    Neighbors        |
34 | 33 | rspcva 3134 |
. . . . . . . 8
     
            Neighbors      Neighbors      
     Neighbors      Neighbors       |
35 | | ssnid 3989 |
. . . . . . . . . . . . . . 15
   |
36 | | eleq2 2538 |
. . . . . . . . . . . . . . . . 17
        Neighbors      Neighbors           Neighbors 
    Neighbors      |
37 | 36 | eqcoms 2479 |
. . . . . . . . . . . . . . . 16
      Neighbors      Neighbors             Neighbors 
    Neighbors      |
38 | | elin 3608 |
. . . . . . . . . . . . . . . . 17
    
 Neighbors 
    Neighbors        Neighbors      Neighbors     |
39 | 38 | biimpi 199 |
. . . . . . . . . . . . . . . 16
    
 Neighbors 
    Neighbors  
     Neighbors      Neighbors     |
40 | 37, 39 | syl6bi 236 |
. . . . . . . . . . . . . . 15
      Neighbors      Neighbors             Neighbors      Neighbors      |
41 | 35, 40 | mpi 20 |
. . . . . . . . . . . . . 14
      Neighbors      Neighbors        
 Neighbors 
    Neighbors     |
42 | | nbgraeledg 25237 |
. . . . . . . . . . . . . . . . . . . . . 22
 USGrph      Neighbors 
      |
43 | | prcom 4041 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
44 | 43 | eleq1i 2540 |
. . . . . . . . . . . . . . . . . . . . . 22
   
     |
45 | 42, 44 | syl6bb 269 |
. . . . . . . . . . . . . . . . . . . . 21
 USGrph      Neighbors 
      |
46 | 45 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . 20
 USGrph      Neighbors        |
47 | 7, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
      Neighbors 
      |
48 | 47 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
    
 Neighbors 
      |
49 | 48 | com12 31 |
. . . . . . . . . . . . . . . . 17
     Neighbors   
       |
50 | 49 | adantr 472 |
. . . . . . . . . . . . . . . 16
    
 Neighbors 
    Neighbors    
   
   |
51 | 50 | imp 436 |
. . . . . . . . . . . . . . 15
       Neighbors 
    Neighbors        
  |
52 | 1 | eqcomi 2480 |
. . . . . . . . . . . . . . . . . . 19
  
 Neighbors   |
53 | 52 | eleq2i 2541 |
. . . . . . . . . . . . . . . . . 18
     Neighbors 
  |
54 | 53 | biimpi 199 |
. . . . . . . . . . . . . . . . 17
     Neighbors    |
55 | 54 | adantl 473 |
. . . . . . . . . . . . . . . 16
    
 Neighbors 
    Neighbors  
  |
56 | 3, 1, 12, 13, 14, 15, 5, 16 | frgrancvvdeqlem3 25839 |
. . . . . . . . . . . . . . . 16
 
 
     |
57 | | preq2 4043 |
. . . . . . . . . . . . . . . . . 18
         |
58 | 57 | eleq1d 2533 |
. . . . . . . . . . . . . . . . 17
           |
59 | 58 | riota2 6292 |
. . . . . . . . . . . . . . . 16
  
   
   
         |
60 | 55, 56, 59 | syl2an 485 |
. . . . . . . . . . . . . . 15
       Neighbors 
    Neighbors                   |
61 | 51, 60 | mpbid 215 |
. . . . . . . . . . . . . 14
       Neighbors 
    Neighbors              |
62 | 41, 61 | sylan 479 |
. . . . . . . . . . . . 13
       Neighbors      Neighbors                |
63 | 62 | eqcomd 2477 |
. . . . . . . . . . . 12
       Neighbors      Neighbors                |
64 | 63 | sneqd 3971 |
. . . . . . . . . . 11
       Neighbors      Neighbors         
          |
65 | | eqeq1 2475 |
. . . . . . . . . . . 12
      Neighbors      Neighbors           Neighbors      Neighbors          
 
           |
66 | 65 | adantr 472 |
. . . . . . . . . . 11
       Neighbors      Neighbors              Neighbors      Neighbors          
 
           |
67 | 64, 66 | mpbird 240 |
. . . . . . . . . 10
       Neighbors      Neighbors             Neighbors      Neighbors             |
68 | 67 | ex 441 |
. . . . . . . . 9
      Neighbors      Neighbors      
      Neighbors      Neighbors              |
69 | 68 | rexlimivw 2869 |
. . . . . . . 8
       Neighbors      Neighbors      
      Neighbors      Neighbors              |
70 | 34, 69 | syl 17 |
. . . . . . 7
     
            Neighbors      Neighbors       
      Neighbors      Neighbors              |
71 | 70 | expcom 442 |
. . . . . 6
 
           Neighbors      Neighbors     
          
 Neighbors 
    Neighbors     
         |
72 | 29, 71 | syl 17 |
. . . . 5
   
           Neighbors      Neighbors            
      Neighbors      Neighbors               |
73 | 72 | impancom 447 |
. . . 4
 
    
 

           Neighbors      Neighbors      
      Neighbors      Neighbors               |
74 | 73 | imp 436 |
. . 3
  
     

           Neighbors      Neighbors       
      Neighbors      Neighbors              |
75 | 21, 74 | mpcom 36 |
. 2
 
      Neighbors      Neighbors             |
76 | 2, 75 | syl5req 2518 |
1
 
   
          Neighbors     |