Step | Hyp | Ref
| Expression |
1 | | rusgraprop 25650 |
. . . . 5
  
 RegUSGrph  USGrph

  VDeg
       |
2 | | nn0re 10875 |
. . . . . . . . . 10

  |
3 | | 1re 9639 |
. . . . . . . . . 10
 |
4 | | lenlt 9709 |
. . . . . . . . . . 11
 
     |
5 | 4 | bicomd 205 |
. . . . . . . . . 10
 
 
   |
6 | 2, 3, 5 | sylancl 667 |
. . . . . . . . 9


   |
7 | | ioran 493 |
. . . . . . . . . . 11
   
   |
8 | | df-ne 2623 |
. . . . . . . . . . . . 13

  |
9 | | elnnne0 10880 |
. . . . . . . . . . . . . . . 16

    |
10 | | nnle1eq1 10634 |
. . . . . . . . . . . . . . . . 17
 
   |
11 | | rusgrasn 25666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         RegUSGrph 
  |
12 | 11 | orcd 394 |
. . . . . . . . . . . . . . . . . . . . . . 23
         RegUSGrph 
    |
13 | 12 | expcom 437 |
. . . . . . . . . . . . . . . . . . . . . 22
  
 RegUSGrph           |
14 | 13 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
     RegUSGrph
FriendGrph            |
15 | 14 | com12 32 |
. . . . . . . . . . . . . . . . . . . 20
          RegUSGrph
FriendGrph       |
16 | 15 | a1d 26 |
. . . . . . . . . . . . . . . . . . 19
             RegUSGrph FriendGrph        |
17 | 16 | a1d 26 |
. . . . . . . . . . . . . . . . . 18
     
        RegUSGrph FriendGrph         |
18 | | hashcl 12535 |
. . . . . . . . . . . . . . . . . . . . 21
       |
19 | | rusisusgra 25652 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
 RegUSGrph USGrph   |
20 | | usgrav 25058 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 USGrph 
   |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
 RegUSGrph     |
22 | | hasheq0 12541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
   |
23 | 22 | bicomd 205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
       |
24 | 23 | necon3bid 2667 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
25 | | elnnne0 10880 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
                 |
26 | | df-ne 2623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
    
      |
27 | | eluz2b3 11229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
                     |
28 | | eluz2 11162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
                     |
29 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
             |
30 | | 2re 10676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 |
31 | 30 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
             |
32 | | zre 10938 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
    
      |
33 | 32 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
                 |
34 | | 1lt2 10773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
    
  |
36 | 35 | anim1i 571 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
           
       |
37 | | ltletr 9722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
 
      
    
       |
38 | 37 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
        
            |
39 | 29, 31, 33, 36, 38 | syl31anc 1270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
                 |
40 | | eqeq2 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
    VDeg    
  VDeg        |
41 | 40 | ralbidv 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
  
  VDeg    
   VDeg        |
42 | 41 | ad2antll 734 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
  FriendGrph
              
  VDeg    

  VDeg        |
43 | | vdgn1frgrav3 25749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . 59
  FriendGrph
     
  VDeg       |
44 | | r19.26 2916 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . 61
 
   VDeg    
  VDeg
      
  VDeg        VDeg        |
45 | | df-ne 2623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
   VDeg    
  VDeg       |
46 | 45 | anbi1i 700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
    VDeg    
  VDeg
        VDeg
      VDeg        |
47 | | ancom 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
    VDeg       VDeg     
   VDeg
      VDeg        |
48 | | pm3.24 892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
   VDeg       VDeg       |
49 | 48 | bifal 1456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
    VDeg       VDeg     
 |
50 | 46, 47, 49 | 3bitri 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
    VDeg    
  VDeg
    
 |
51 | 50 | ralbii 2818 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
 
   VDeg    
  VDeg
       |
52 | | r19.3rzv 3861 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

   |
53 | | falim 1457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
    |
54 | 52, 53 | syl6bir 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63

 
     |
55 | 54 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
 
 
    |
56 | 51, 55 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . 61
 
   VDeg    
  VDeg
    

     |
57 | 44, 56 | sylbir 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . 60
     VDeg    

  VDeg            |
58 | 57 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . 59
 
  VDeg
        VDeg      
     |
59 | 43, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . 58
  FriendGrph
      
  VDeg     
      |
60 | 59 | expcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
    
 FriendGrph  
  VDeg      
      |
61 | 60 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
             
FriendGrph  
  VDeg     
       |
62 | 61 | impcom 432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
  FriendGrph
              
  VDeg      
     |
63 | 42, 62 | sylbid 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
  FriendGrph
              
  VDeg      
     |
64 | 63 | com23 81 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
  FriendGrph
               
  VDeg           |
65 | 64 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
 FriendGrph                
  VDeg    
       |
66 | 65 | com24 90 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
 FriendGrph  
  VDeg                 
        |
67 | 66 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
 
  VDeg
     FriendGrph             
        |
68 | 67 | 3ad2ant3 1030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
  USGrph

  VDeg       FriendGrph             
        |
69 | 1, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
  
 RegUSGrph  FriendGrph
            
        |
70 | 69 | impcom 432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
  FriendGrph
   RegUSGrph  
                   |
71 | 70 | impcom 432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
   FriendGrph    RegUSGrph                
    |
72 | 71 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
                FriendGrph  
 RegUSGrph   
    |
73 | 72 | ex 436 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
           
   FriendGrph    RegUSGrph         |
74 | 39, 73 | syldan 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
           
   FriendGrph    RegUSGrph         |
75 | 74 | 3adant1 1025 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
           
   FriendGrph    RegUSGrph         |
76 | 28, 75 | sylbi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
             FriendGrph    RegUSGrph         |
77 | 27, 76 | sylbir 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
               FriendGrph    RegUSGrph         |
78 | 77 | expcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
    
    
    FriendGrph    RegUSGrph          |
79 | 78 | com23 81 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
    
         FriendGrph    RegUSGrph          |
80 | 26, 79 | sylbir 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
              FriendGrph  
 RegUSGrph   
      |
81 | 80 | com13 83 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
    
         FriendGrph  
 RegUSGrph   
      |
82 | 25, 81 | sylbir 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                
   FriendGrph    RegUSGrph          |
83 | 82 | expcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
    
    
         FriendGrph  
 RegUSGrph   
       |
84 | 83 | com25 94 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
   FriendGrph    RegUSGrph        
             |
85 | 84 | expd 438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    

  FriendGrph    RegUSGrph  
                   |
86 | 24, 85 | syl6bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 

  FriendGrph    RegUSGrph  
                    |
87 | 86 | com13 83 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30



  FriendGrph    RegUSGrph  
                    |
88 | 87 | pm2.43i 49 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29


  FriendGrph    RegUSGrph  
                   |
89 | 88 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    
FriendGrph    RegUSGrph  
         
        |
90 | 89 | expd 438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    FriendGrph
    RegUSGrph      
              |
91 | 90 | expcom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
 FriendGrph     RegUSGrph
                     |
92 | 91 | com24 90 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     RegUSGrph  FriendGrph
 
                    |
93 | 92 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     RegUSGrph  FriendGrph  
                    |
94 | 21, 93 | mpcom 37 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
 RegUSGrph  FriendGrph
 
                   |
95 | 94 | imp 431 |
. . . . . . . . . . . . . . . . . . . . . 22
     RegUSGrph
FriendGrph   
                  |
96 | 95 | com15 96 |
. . . . . . . . . . . . . . . . . . . . 21
    

           RegUSGrph FriendGrph          |
97 | 18, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
           RegUSGrph FriendGrph          |
98 | 97 | imp 431 |
. . . . . . . . . . . . . . . . . . 19
   
          RegUSGrph FriendGrph         |
99 | 98 | com13 83 |
. . . . . . . . . . . . . . . . . 18
              RegUSGrph
FriendGrph         |
100 | 17, 99 | pm2.61i 168 |
. . . . . . . . . . . . . . . . 17
         RegUSGrph FriendGrph        |
101 | 10, 100 | syl6bi 232 |
. . . . . . . . . . . . . . . 16
          RegUSGrph FriendGrph         |
102 | 9, 101 | sylbir 217 |
. . . . . . . . . . . . . . 15
     

     RegUSGrph
FriendGrph         |
103 | 102 | expcom 437 |
. . . . . . . . . . . . . 14
 
         RegUSGrph FriendGrph          |
104 | 103 | com23 81 |
. . . . . . . . . . . . 13
  
        RegUSGrph FriendGrph          |
105 | 8, 104 | sylbir 217 |
. . . . . . . . . . . 12
    

     RegUSGrph
FriendGrph          |
106 | 105 | adantr 467 |
. . . . . . . . . . 11
    
        RegUSGrph FriendGrph          |
107 | 7, 106 | sylbi 199 |
. . . . . . . . . 10
  


 
      RegUSGrph
FriendGrph          |
108 | 107 | com13 83 |
. . . . . . . . 9

   
 
      RegUSGrph
FriendGrph          |
109 | 6, 108 | sylbid 219 |
. . . . . . . 8

     

     RegUSGrph
FriendGrph          |
110 | 109 | com25 94 |
. . . . . . 7

     RegUSGrph
FriendGrph      

 
       |
111 | 110 | 3ad2ant2 1029 |
. . . . . 6
  USGrph

  VDeg         
 RegUSGrph
FriendGrph      

 
       |
112 | 111 | expd 438 |
. . . . 5
  USGrph

  VDeg          RegUSGrph
 FriendGrph  
    
         |
113 | 1, 112 | mpcom 37 |
. . . 4
  
 RegUSGrph  FriendGrph
      
        |
114 | 113 | impcom 432 |
. . 3
  FriendGrph
   RegUSGrph    
 
 
       |
115 | 114 | com14 91 |
. 2
     

  FriendGrph    RegUSGrph  
      |
116 | | simprl 763 |
. . . . 5
       FriendGrph  
 RegUSGrph   FriendGrph   |
117 | | simpl 459 |
. . . . . 6
     |
118 | 117 | ad2antlr 732 |
. . . . 5
       FriendGrph  
 RegUSGrph     |
119 | | simpr 463 |
. . . . . 6
     |
120 | 119 | ad2antlr 732 |
. . . . 5
       FriendGrph  
 RegUSGrph     |
121 | | simpl 459 |
. . . . . 6
  
    |
122 | | simpr 463 |
. . . . . 6
  FriendGrph
   RegUSGrph     RegUSGrph   |
123 | 121, 122 | anim12ci 570 |
. . . . 5
       FriendGrph  
 RegUSGrph       RegUSGrph
   |
124 | | frgrareggt1 25837 |
. . . . . 6
  FriendGrph

     RegUSGrph
    |
125 | 124 | imp 431 |
. . . . 5
   FriendGrph
     RegUSGrph
 
  |
126 | 116, 118,
120, 123, 125 | syl31anc 1270 |
. . . 4
       FriendGrph  
 RegUSGrph     |
127 | 126 | olcd 395 |
. . 3
       FriendGrph  
 RegUSGrph   
   |
128 | 127 | exp31 608 |
. 2
      FriendGrph  
 RegUSGrph 
      |
129 | | 2a1 28 |
. 2
       
FriendGrph    RegUSGrph        |
130 | 115, 128,
129 | pm2.61ii 169 |
1
    
FriendGrph    RegUSGrph       |