Proof of Theorem nb3graprlem2
Step | Hyp | Ref
| Expression |
1 | | sneq 3980 |
. . . . . 6
       |
2 | 1 | difeq2d 3553 |
. . . . 5
     
             |
3 | | preq1 4054 |
. . . . . 6
         |
4 | 3 | eqeq2d 2463 |
. . . . 5
      Neighbors         Neighbors        |
5 | 2, 4 | rexeqbidv 3004 |
. . . 4
  
    
      
 Neighbors    
    
         Neighbors   
    |
6 | | sneq 3980 |
. . . . . 6
       |
7 | 6 | difeq2d 3553 |
. . . . 5
     
             |
8 | | preq1 4054 |
. . . . . 6
         |
9 | 8 | eqeq2d 2463 |
. . . . 5
      Neighbors         Neighbors        |
10 | 7, 9 | rexeqbidv 3004 |
. . . 4
  
    
      
 Neighbors    
    
         Neighbors   
    |
11 | | sneq 3980 |
. . . . . 6
       |
12 | 11 | difeq2d 3553 |
. . . . 5
     
             |
13 | | preq1 4054 |
. . . . . 6
         |
14 | 13 | eqeq2d 2463 |
. . . . 5
      Neighbors         Neighbors        |
15 | 12, 14 | rexeqbidv 3004 |
. . . 4
  
    
      
 Neighbors    
    
         Neighbors   
    |
16 | 5, 10, 15 | rextpg 4026 |
. . 3
 
            
         Neighbors                  
 Neighbors     
  
 
      
 Neighbors     
  
 
      
 Neighbors         |
17 | 16 | 3ad2ant1 1030 |
. 2
  

     USGrph                
         Neighbors                  
 Neighbors     
  
 
      
 Neighbors     
  
 
      
 Neighbors         |
18 | | simpl 459 |
. . . 4
     
USGrph 
      |
19 | | difeq1 3546 |
. . . . . 6
   
        
      |
20 | 19 | adantr 467 |
. . . . 5
     
USGrph         
      |
21 | 20 | rexeqdv 2996 |
. . . 4
     
USGrph             Neighbors    
    
         Neighbors        |
22 | 18, 21 | rexeqbidv 3004 |
. . 3
     
USGrph              Neighbors    
          
         Neighbors        |
23 | 22 | 3ad2ant2 1031 |
. 2
  

     USGrph                 Neighbors    
          
         Neighbors        |
24 | | preq2 4055 |
. . . . . . . 8
     
   |
25 | 24 | eqeq2d 2463 |
. . . . . . 7
      Neighbors   
     Neighbors        |
26 | | preq2 4055 |
. . . . . . . 8
     
   |
27 | 26 | eqeq2d 2463 |
. . . . . . 7
      Neighbors   
     Neighbors        |
28 | 25, 27 | rexprg 4024 |
. . . . . 6
 
          Neighbors   
      Neighbors   
     Neighbors   
     |
29 | 28 | 3adant1 1027 |
. . . . 5
 
          Neighbors   
      Neighbors   
     Neighbors   
     |
30 | | preq2 4055 |
. . . . . . . . 9
     
   |
31 | 30 | eqeq2d 2463 |
. . . . . . . 8
      Neighbors   
     Neighbors        |
32 | | preq2 4055 |
. . . . . . . . 9
     
   |
33 | 32 | eqeq2d 2463 |
. . . . . . . 8
      Neighbors   
     Neighbors        |
34 | 31, 33 | rexprg 4024 |
. . . . . . 7
 
          Neighbors   
      Neighbors   
     Neighbors   
     |
35 | 34 | ancoms 455 |
. . . . . 6
 
          Neighbors   
      Neighbors   
     Neighbors   
     |
36 | 35 | 3adant2 1028 |
. . . . 5
 
          Neighbors   
      Neighbors   
     Neighbors   
     |
37 | | preq2 4055 |
. . . . . . . 8
     
   |
38 | 37 | eqeq2d 2463 |
. . . . . . 7
      Neighbors   
     Neighbors        |
39 | | preq2 4055 |
. . . . . . . 8
     
   |
40 | 39 | eqeq2d 2463 |
. . . . . . 7
      Neighbors   
     Neighbors        |
41 | 38, 40 | rexprg 4024 |
. . . . . 6
 
          Neighbors   
      Neighbors   
     Neighbors   
     |
42 | 41 | 3adant3 1029 |
. . . . 5
 
          Neighbors   
      Neighbors   
     Neighbors   
     |
43 | 29, 36, 42 | 3orbi123d 1340 |
. . . 4
 
           Neighbors   
   
     Neighbors   
   
     Neighbors   
        Neighbors         Neighbors           Neighbors   
     Neighbors   
       Neighbors         Neighbors          |
44 | 43 | 3ad2ant1 1030 |
. . 3
  

     USGrph               Neighbors   
   
     Neighbors   
   
     Neighbors   
        Neighbors         Neighbors           Neighbors   
     Neighbors   
       Neighbors         Neighbors          |
45 | | tprot 4070 |
. . . . . . . . 9
         |
46 | 45 | a1i 11 |
. . . . . . . 8
             |
47 | 46 | difeq1d 3552 |
. . . . . . 7
       
             |
48 | | necom 2679 |
. . . . . . . . 9

  |
49 | | necom 2679 |
. . . . . . . . 9

  |
50 | | diftpsn3 4113 |
. . . . . . . . 9
      
         |
51 | 48, 49, 50 | syl2anb 482 |
. . . . . . . 8
      
         |
52 | 51 | 3adant3 1029 |
. . . . . . 7
       
    
   |
53 | 47, 52 | eqtrd 2487 |
. . . . . 6
       
    
   |
54 | 53 | rexeqdv 2996 |
. . . . 5
    
    
      
 Neighbors    
        Neighbors   
    |
55 | | tprot 4070 |
. . . . . . . . . 10
         |
56 | 55 | eqcomi 2462 |
. . . . . . . . 9
         |
57 | 56 | a1i 11 |
. . . . . . . 8
             |
58 | 57 | difeq1d 3552 |
. . . . . . 7
       
             |
59 | | necom 2679 |
. . . . . . . . . . . 12

  |
60 | 59 | anbi1i 702 |
. . . . . . . . . . 11
  
    |
61 | 60 | biimpi 198 |
. . . . . . . . . 10
   
   |
62 | 61 | ancoms 455 |
. . . . . . . . 9
   
   |
63 | | diftpsn3 4113 |
. . . . . . . . 9
      
         |
64 | 62, 63 | syl 17 |
. . . . . . . 8
      
         |
65 | 64 | 3adant2 1028 |
. . . . . . 7
       
    
   |
66 | 58, 65 | eqtrd 2487 |
. . . . . 6
       
    
   |
67 | 66 | rexeqdv 2996 |
. . . . 5
    
    
      
 Neighbors    
        Neighbors   
    |
68 | | diftpsn3 4113 |
. . . . . . 7
      
         |
69 | 68 | 3adant1 1027 |
. . . . . 6
       
    
   |
70 | 69 | rexeqdv 2996 |
. . . . 5
    
    
      
 Neighbors    
        Neighbors   
    |
71 | 54, 67, 70 | 3orbi123d 1340 |
. . . 4
         
         Neighbors   
             
 Neighbors     
  
 
      
 Neighbors     
 
     
 Neighbors     
     
 Neighbors     
     
 Neighbors         |
72 | 71 | 3ad2ant3 1032 |
. . 3
  

     USGrph           
         Neighbors   
             
 Neighbors     
  
 
      
 Neighbors     
 
     
 Neighbors     
     
 Neighbors     
     
 Neighbors         |
73 | | prcom 4053 |
. . . . . . . 8
    
  |
74 | 73 | eqeq2i 2465 |
. . . . . . 7
     Neighbors    
    Neighbors       |
75 | 74 | orbi2i 522 |
. . . . . 6
      Neighbors   
     Neighbors   
     
 Neighbors         Neighbors        |
76 | | oridm 517 |
. . . . . 6
      Neighbors   
     Neighbors   
      Neighbors   
   |
77 | 75, 76 | bitr2i 254 |
. . . . 5
     Neighbors    
     Neighbors         Neighbors        |
78 | 77 | a1i 11 |
. . . 4
  

     USGrph          Neighbors   
      Neighbors   
     Neighbors   
     |
79 | | nbgranself2 25176 |
. . . . . . . . . 10
 USGrph     Neighbors    |
80 | | df-nel 2627 |
. . . . . . . . . . 11
     Neighbors 
    Neighbors    |
81 | | prid2g 4082 |
. . . . . . . . . . . . . 14
      |
82 | 81 | 3ad2ant1 1030 |
. . . . . . . . . . . . 13
 
      |
83 | | eleq2 2520 |
. . . . . . . . . . . . 13
     Neighbors     
    Neighbors        |
84 | 82, 83 | syl5ibrcom 226 |
. . . . . . . . . . . 12
 
      Neighbors   
   
 Neighbors     |
85 | 84 | con3rr3 142 |
. . . . . . . . . . 11
   
 Neighbors 
 
     Neighbors   
    |
86 | 80, 85 | sylbi 199 |
. . . . . . . . . 10
     Neighbors   

    Neighbors        |
87 | 79, 86 | syl 17 |
. . . . . . . . 9
 USGrph  
     Neighbors   
    |
88 | 87 | adantl 468 |
. . . . . . . 8
     
USGrph         Neighbors   
    |
89 | 88 | impcom 432 |
. . . . . . 7
  

     USGrph       Neighbors   
   |
90 | 89 | 3adant3 1029 |
. . . . . 6
  

     USGrph         Neighbors   
   |
91 | | biorf 407 |
. . . . . . 7
     Neighbors   
      Neighbors   
      Neighbors   
     Neighbors   
     |
92 | | orcom 389 |
. . . . . . 7
      Neighbors   
     Neighbors   
     
 Neighbors         Neighbors        |
93 | 91, 92 | syl6bb 265 |
. . . . . 6
     Neighbors   
      Neighbors   
      Neighbors   
     Neighbors   
     |
94 | 90, 93 | syl 17 |
. . . . 5
  

     USGrph          Neighbors   
      Neighbors   
     Neighbors   
     |
95 | | prid2g 4082 |
. . . . . . . . . . . . . 14
      |
96 | 95 | 3ad2ant1 1030 |
. . . . . . . . . . . . 13
 
      |
97 | | eleq2 2520 |
. . . . . . . . . . . . 13
     Neighbors     
    Neighbors        |
98 | 96, 97 | syl5ibrcom 226 |
. . . . . . . . . . . 12
 
      Neighbors   
   
 Neighbors     |
99 | 98 | con3rr3 142 |
. . . . . . . . . . 11
   
 Neighbors 
 
     Neighbors   
    |
100 | 80, 99 | sylbi 199 |
. . . . . . . . . 10
     Neighbors   

    Neighbors        |
101 | 79, 100 | syl 17 |
. . . . . . . . 9
 USGrph  
     Neighbors   
    |
102 | 101 | adantl 468 |
. . . . . . . 8
     
USGrph         Neighbors   
    |
103 | 102 | impcom 432 |
. . . . . . 7
  

     USGrph       Neighbors   
   |
104 | 103 | 3adant3 1029 |
. . . . . 6
  

     USGrph         Neighbors   
   |
105 | | biorf 407 |
. . . . . 6
     Neighbors   
      Neighbors   
      Neighbors   
     Neighbors   
     |
106 | 104, 105 | syl 17 |
. . . . 5
  

     USGrph          Neighbors   
      Neighbors   
     Neighbors   
     |
107 | 94, 106 | orbi12d 717 |
. . . 4
  

     USGrph         
 Neighbors         Neighbors     
      Neighbors   
     Neighbors   
       Neighbors         Neighbors          |
108 | | prid1g 4081 |
. . . . . . . . . . . . . . . 16
      |
109 | 108 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . 15
 
      |
110 | | eleq2 2520 |
. . . . . . . . . . . . . . 15
     Neighbors     
    Neighbors        |
111 | 109, 110 | syl5ibrcom 226 |
. . . . . . . . . . . . . 14
 
      Neighbors   
   
 Neighbors     |
112 | 111 | con3dimp 443 |
. . . . . . . . . . . . 13
  

    Neighbors       Neighbors   
   |
113 | | prid1g 4081 |
. . . . . . . . . . . . . . . 16
      |
114 | 113 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . 15
 
      |
115 | | eleq2 2520 |
. . . . . . . . . . . . . . 15
     Neighbors     
    Neighbors        |
116 | 114, 115 | syl5ibrcom 226 |
. . . . . . . . . . . . . 14
 
      Neighbors   
   
 Neighbors     |
117 | 116 | con3dimp 443 |
. . . . . . . . . . . . 13
  

    Neighbors       Neighbors   
   |
118 | 112, 117 | jca 535 |
. . . . . . . . . . . 12
  

    Neighbors      
 Neighbors         Neighbors   
    |
119 | 118 | expcom 437 |
. . . . . . . . . . 11
   
 Neighbors 
 
    
 Neighbors         Neighbors   
     |
120 | 80, 119 | sylbi 199 |
. . . . . . . . . 10
     Neighbors   

     Neighbors   
     Neighbors   
     |
121 | 79, 120 | syl 17 |
. . . . . . . . 9
 USGrph  
      Neighbors   
     Neighbors   
     |
122 | 121 | adantl 468 |
. . . . . . . 8
     
USGrph          Neighbors   
     Neighbors   
     |
123 | 122 | impcom 432 |
. . . . . . 7
  

     USGrph        Neighbors   
     Neighbors   
    |
124 | 123 | 3adant3 1029 |
. . . . . 6
  

     USGrph        
 Neighbors         Neighbors   
    |
125 | | ioran 493 |
. . . . . 6
      Neighbors   
     Neighbors   
       Neighbors         Neighbors   
    |
126 | 124, 125 | sylibr 216 |
. . . . 5
  

     USGrph          Neighbors   
     Neighbors   
    |
127 | 126 | 3bior1fd 1377 |
. . . 4
  

     USGrph            Neighbors         Neighbors           Neighbors   
     Neighbors   
  
      Neighbors   
     Neighbors   
       Neighbors         Neighbors           Neighbors   
     Neighbors   
      |
128 | 78, 107, 127 | 3bitrd 283 |
. . 3
  

     USGrph          Neighbors   
       Neighbors   
     Neighbors   
       Neighbors         Neighbors           Neighbors   
     Neighbors   
      |
129 | 44, 72, 128 | 3bitr4rd 290 |
. 2
  

     USGrph          Neighbors   
              
 Neighbors     
  
 
      
 Neighbors     
  
 
      
 Neighbors         |
130 | 17, 23, 129 | 3bitr4rd 290 |
1
  

     USGrph          Neighbors   
  
         Neighbors        |