Step | Hyp | Ref
| Expression |
1 | | usgrav 25058 |
. . . . . 6
    
USGrph     
   |
2 | | isfrgra 25711 |
. . . . . 6
          
 FriendGrph    
 USGrph           
       
 
             |
3 | 1, 2 | syl 17 |
. . . . 5
    
USGrph     
FriendGrph
  
 
USGrph 
     
    
                      |
4 | 3 | adantl 468 |
. . . 4
           
USGrph     
 FriendGrph    
 USGrph           
       
 
             |
5 | | ibar 507 |
. . . . 5
    
USGrph  
     
    
                       USGrph           
       
 
             |
6 | 5 | adantl 468 |
. . . 4
           
USGrph             
       
 
            
 USGrph           
       
 
             |
7 | 4, 6 | bitr4d 260 |
. . 3
           
USGrph     
 FriendGrph 
     
    
                     |
8 | | sneq 3977 |
. . . . . . . . 9
       |
9 | 8 | difeq2d 3550 |
. . . . . . . 8
     
             |
10 | | preq2 4051 |
. . . . . . . . . . 11
         |
11 | 10 | preq1d 4056 |
. . . . . . . . . 10
              
      |
12 | 11 | sseq1d 3458 |
. . . . . . . . 9
          
        
   |
13 | 12 | reubidv 2974 |
. . . . . . . 8
  
            
  
 
        
   |
14 | 9, 13 | raleqbidv 3000 |
. . . . . . 7
  
    
                                             |
15 | | sneq 3977 |
. . . . . . . . 9
       |
16 | 15 | difeq2d 3550 |
. . . . . . . 8
     
             |
17 | | preq2 4051 |
. . . . . . . . . . 11
         |
18 | 17 | preq1d 4056 |
. . . . . . . . . 10
              
      |
19 | 18 | sseq1d 3458 |
. . . . . . . . 9
          
        
   |
20 | 19 | reubidv 2974 |
. . . . . . . 8
  
            
  
 
        
   |
21 | 16, 20 | raleqbidv 3000 |
. . . . . . 7
  
    
                                             |
22 | | sneq 3977 |
. . . . . . . . 9
       |
23 | 22 | difeq2d 3550 |
. . . . . . . 8
     
             |
24 | | preq2 4051 |
. . . . . . . . . . 11
         |
25 | 24 | preq1d 4056 |
. . . . . . . . . 10
              
      |
26 | 25 | sseq1d 3458 |
. . . . . . . . 9
          
        
   |
27 | 26 | reubidv 2974 |
. . . . . . . 8
  
            
  
 
        
   |
28 | 23, 27 | raleqbidv 3000 |
. . . . . . 7
  
    
                                             |
29 | 14, 21, 28 | raltpg 4022 |
. . . . . 6
 
            
       
 
              
       
 
        
     
                      
       
 
        
    |
30 | 29 | adantr 467 |
. . . . 5
  


   
     
    
                       
       
 
        
     
                      
       
 
        
    |
31 | 30 | adantr 467 |
. . . 4
           
USGrph             
       
 
              
       
 
        
     
                      
       
 
        
    |
32 | | tprot 4066 |
. . . . . . . . . . 11
         |
33 | 32 | a1i 11 |
. . . . . . . . . 10
             |
34 | 33 | difeq1d 3549 |
. . . . . . . . 9
       
             |
35 | | necom 2676 |
. . . . . . . . . . . . 13

  |
36 | 35 | biimpi 198 |
. . . . . . . . . . . 12
   |
37 | | necom 2676 |
. . . . . . . . . . . . 13

  |
38 | 37 | biimpi 198 |
. . . . . . . . . . . 12
   |
39 | 36, 38 | anim12i 569 |
. . . . . . . . . . 11
   
   |
40 | 39 | 3adant3 1027 |
. . . . . . . . . 10
       |
41 | | diftpsn3 4109 |
. . . . . . . . . 10
      
         |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
       
    
   |
43 | 34, 42 | eqtrd 2484 |
. . . . . . . 8
       
    
   |
44 | 43 | raleqdv 2992 |
. . . . . . 7
    
    
                  
                     |
45 | | tprot 4066 |
. . . . . . . . . . . 12
         |
46 | 45 | eqcomi 2459 |
. . . . . . . . . . 11
         |
47 | 46 | a1i 11 |
. . . . . . . . . 10
             |
48 | 47 | difeq1d 3549 |
. . . . . . . . 9
       
             |
49 | | id 22 |
. . . . . . . . . . . 12
   |
50 | | necom 2676 |
. . . . . . . . . . . . 13

  |
51 | 50 | biimpi 198 |
. . . . . . . . . . . 12
   |
52 | 49, 51 | anim12ci 570 |
. . . . . . . . . . 11
   
   |
53 | 52 | 3adant2 1026 |
. . . . . . . . . 10
       |
54 | | diftpsn3 4109 |
. . . . . . . . . 10
      
         |
55 | 53, 54 | syl 17 |
. . . . . . . . 9
       
    
   |
56 | 48, 55 | eqtrd 2484 |
. . . . . . . 8
       
    
   |
57 | 56 | raleqdv 2992 |
. . . . . . 7
    
    
                  
                     |
58 | | diftpsn3 4109 |
. . . . . . . . 9
      
         |
59 | 58 | 3adant1 1025 |
. . . . . . . 8
       
    
   |
60 | 59 | raleqdv 2992 |
. . . . . . 7
    
    
                  
                     |
61 | 44, 57, 60 | 3anbi123d 1338 |
. . . . . 6
         
       
 
        
     
                      
       
 
        
         
 
        
                          
 
        
    |
62 | 61 | adantl 468 |
. . . . 5
  


        
       
 
        
     
                      
       
 
        
         
 
        
                          
 
        
    |
63 | 62 | adantr 467 |
. . . 4
           
USGrph        
       
 
        
     
                      
       
 
        
         
 
        
                          
 
        
    |
64 | | preq2 4051 |
. . . . . . . . . . . 12
         |
65 | 64 | preq2d 4057 |
. . . . . . . . . . 11
              
      |
66 | 65 | sseq1d 3458 |
. . . . . . . . . 10
      
   
            |
67 | 66 | reubidv 2974 |
. . . . . . . . 9
  
        
   
  
 
            |
68 | | preq2 4051 |
. . . . . . . . . . . 12
         |
69 | 68 | preq2d 4057 |
. . . . . . . . . . 11
              
      |
70 | 69 | sseq1d 3458 |
. . . . . . . . . 10
      
   
            |
71 | 70 | reubidv 2974 |
. . . . . . . . 9
  
        
   
  
 
            |
72 | 67, 71 | ralprg 4020 |
. . . . . . . 8
 
         
 
        
 
        
                 
    |
73 | 72 | 3adant1 1025 |
. . . . . . 7
 
         
 
        
 
        
                 
    |
74 | 68 | preq2d 4057 |
. . . . . . . . . . . 12
              
      |
75 | 74 | sseq1d 3458 |
. . . . . . . . . . 11
      
   
            |
76 | 75 | reubidv 2974 |
. . . . . . . . . 10
  
        
   
  
 
            |
77 | | preq2 4051 |
. . . . . . . . . . . . 13
         |
78 | 77 | preq2d 4057 |
. . . . . . . . . . . 12
              
      |
79 | 78 | sseq1d 3458 |
. . . . . . . . . . 11
      
   
            |
80 | 79 | reubidv 2974 |
. . . . . . . . . 10
  
        
   
  
 
            |
81 | 76, 80 | ralprg 4020 |
. . . . . . . . 9
 
         
 
        
 
        
                 
    |
82 | 81 | ancoms 455 |
. . . . . . . 8
 
         
 
        
 
        
                 
    |
83 | 82 | 3adant2 1026 |
. . . . . . 7
 
         
 
        
 
        
                 
    |
84 | 77 | preq2d 4057 |
. . . . . . . . . . 11
              
      |
85 | 84 | sseq1d 3458 |
. . . . . . . . . 10
      
   
            |
86 | 85 | reubidv 2974 |
. . . . . . . . 9
  
        
   
  
 
            |
87 | 64 | preq2d 4057 |
. . . . . . . . . . 11
              
      |
88 | 87 | sseq1d 3458 |
. . . . . . . . . 10
      
   
            |
89 | 88 | reubidv 2974 |
. . . . . . . . 9
  
        
   
  
 
            |
90 | 86, 89 | ralprg 4020 |
. . . . . . . 8
 
         
 
        
 
        
                 
    |
91 | 90 | 3adant3 1027 |
. . . . . . 7
 
         
 
        
 
        
                 
    |
92 | 73, 83, 91 | 3anbi123d 1338 |
. . . . . 6
 
          
 
        
                          
 
        
                
  
 
                        
  
 
                        
  
 
              |
93 | 92 | adantr 467 |
. . . . 5
  


           
 
        
                          
 
        
                
  
 
                        
  
 
                        
  
 
              |
94 | 93 | adantr 467 |
. . . 4
           
USGrph           
 
        
                          
 
        
                
  
 
                        
  
 
                        
  
 
              |
95 | 31, 63, 94 | 3bitrd 283 |
. . 3
           
USGrph             
       
 
                        
  
 
                        
  
 
                        
  
 
              |
96 | | frgra3vlem2 25722 |
. . . . . . 7
  


      
USGrph  
        
          
     |
97 | 96 | imp 431 |
. . . . . 6
           
USGrph                
   
       |
98 | | 3ancomb 993 |
. . . . . . . 8
 
 
   |
99 | | 3ancoma 991 |
. . . . . . . . 9
  

   |
100 | | biid 240 |
. . . . . . . . . 10

  |
101 | | biid 240 |
. . . . . . . . . 10

  |
102 | 100, 101,
50 | 3anbi123i 1196 |
. . . . . . . . 9
  

   |
103 | 99, 102 | bitri 253 |
. . . . . . . 8
  

   |
104 | 98, 103 | anbi12i 702 |
. . . . . . 7
  


 
 
 
    |
105 | | tpcomb 4068 |
. . . . . . . 8
         |
106 | 105 | breq1i 4408 |
. . . . . . 7
    
USGrph
    USGrph   |
107 | | reueq1 2988 |
. . . . . . . . 9
    
 
 
          
      
 
            |
108 | 105, 107 | mp1i 13 |
. . . . . . . 8
           
USGrph                
         
       |
109 | | frgra3vlem2 25722 |
. . . . . . . . 9
  


      
USGrph  
        
          
     |
110 | 109 | imp 431 |
. . . . . . . 8
           
USGrph                
   
       |
111 | 108, 110 | bitrd 257 |
. . . . . . 7
           
USGrph                
   
       |
112 | 104, 106,
111 | syl2anb 482 |
. . . . . 6
           
USGrph                
   
       |
113 | 97, 112 | anbi12d 716 |
. . . . 5
           
USGrph                 
  
 
                 
      
      |
114 | | 3anrot 989 |
. . . . . . . 8
 
 
   |
115 | | 3anrot 989 |
. . . . . . . . 9
  

   |
116 | | biid 240 |
. . . . . . . . . 10

  |
117 | 116, 35, 37 | 3anbi123i 1196 |
. . . . . . . . 9
  

   |
118 | 115, 117 | bitr3i 255 |
. . . . . . . 8
  

   |
119 | 114, 118 | anbi12i 702 |
. . . . . . 7
  


 
 
 
    |
120 | 32 | breq1i 4408 |
. . . . . . 7
    
USGrph
    USGrph   |
121 | | reueq1 2988 |
. . . . . . . . 9
    
 
 
          
      
 
            |
122 | 32, 121 | mp1i 13 |
. . . . . . . 8
           
USGrph                
         
       |
123 | | frgra3vlem2 25722 |
. . . . . . . . 9
  


      
USGrph  
        
          
     |
124 | 123 | imp 431 |
. . . . . . . 8
           
USGrph                
   
       |
125 | 122, 124 | bitrd 257 |
. . . . . . 7
           
USGrph                
   
       |
126 | 119, 120,
125 | syl2anb 482 |
. . . . . 6
           
USGrph                
   
       |
127 | | 3ancoma 991 |
. . . . . . . 8
 
 
   |
128 | | 3ancomb 993 |
. . . . . . . . 9
  

   |
129 | 35, 116, 100 | 3anbi123i 1196 |
. . . . . . . . 9
  

   |
130 | 128, 129 | bitri 253 |
. . . . . . . 8
  

   |
131 | 127, 130 | anbi12i 702 |
. . . . . . 7
  


 
 
 
    |
132 | | tpcoma 4067 |
. . . . . . . 8
         |
133 | 132 | breq1i 4408 |
. . . . . . 7
    
USGrph
    USGrph   |
134 | | reueq1 2988 |
. . . . . . . . 9
    
 
 
          
      
 
            |
135 | 132, 134 | mp1i 13 |
. . . . . . . 8
           
USGrph                
         
       |
136 | | frgra3vlem2 25722 |
. . . . . . . . 9
  


      
USGrph  
        
          
     |
137 | 136 | imp 431 |
. . . . . . . 8
           
USGrph                
   
       |
138 | 135, 137 | bitrd 257 |
. . . . . . 7
           
USGrph                
   
       |
139 | 131, 133,
138 | syl2anb 482 |
. . . . . 6
           
USGrph                
   
       |
140 | 126, 139 | anbi12d 716 |
. . . . 5
           
USGrph                 
  
 
                 
      
      |
141 | | 3anrot 989 |
. . . . . . . . 9
 
 
   |
142 | 141 | biimpri 210 |
. . . . . . . 8
 
 
   |
143 | | 3anrot 989 |
. . . . . . . . . 10
  

   |
144 | 37, 50, 101 | 3anbi123i 1196 |
. . . . . . . . . 10
  

   |
145 | 143, 144 | bitri 253 |
. . . . . . . . 9
  

   |
146 | 145 | biimpi 198 |
. . . . . . . 8
       |
147 | 142, 146 | anim12i 569 |
. . . . . . 7
  


   


    |
148 | 46 | breq1i 4408 |
. . . . . . . 8
    
USGrph
    USGrph   |
149 | 148 | biimpi 198 |
. . . . . . 7
    
USGrph     USGrph   |
150 | | reueq1 2988 |
. . . . . . . . 9
    
 
 
          
      
 
            |
151 | 46, 150 | mp1i 13 |
. . . . . . . 8
           
USGrph                
         
       |
152 | | frgra3vlem2 25722 |
. . . . . . . . 9
  


      
USGrph  
        
          
     |
153 | 152 | imp 431 |
. . . . . . . 8
           
USGrph                
   
       |
154 | 151, 153 | bitrd 257 |
. . . . . . 7
           
USGrph                
   
       |
155 | 147, 149,
154 | syl2an 480 |
. . . . . 6
           
USGrph                
   
       |
156 | | 3anrev 995 |
. . . . . . . . 9
 
 
   |
157 | 156 | biimpi 198 |
. . . . . . . 8
 
 
   |
158 | 50, 37, 35 | 3anbi123i 1196 |
. . . . . . . . . 10
  

   |
159 | 158 | biimpi 198 |
. . . . . . . . 9
       |
160 | 159 | 3com13 1212 |
. . . . . . . 8
       |
161 | 157, 160 | anim12i 569 |
. . . . . . 7
  


   


    |
162 | | tpcoma 4067 |
. . . . . . . . . 10
         |
163 | 32, 162 | eqtri 2472 |
. . . . . . . . 9
         |
164 | 163 | breq1i 4408 |
. . . . . . . 8
    
USGrph
    USGrph   |
165 | 164 | biimpi 198 |
. . . . . . 7
    
USGrph     USGrph   |
166 | | reueq1 2988 |
. . . . . . . . 9
    
 
 
          
      
 
            |
167 | 163, 166 | mp1i 13 |
. . . . . . . 8
           
USGrph                
         
       |
168 | | frgra3vlem2 25722 |
. . . . . . . . 9
  


      
USGrph  
        
          
     |
169 | 168 | imp 431 |
. . . . . . . 8
           
USGrph                
   
       |
170 | 167, 169 | bitrd 257 |
. . . . . . 7
           
USGrph                
   
       |
171 | 161, 165,
170 | syl2an 480 |
. . . . . 6
           
USGrph                
   
       |
172 | 155, 171 | anbi12d 716 |
. . . . 5
           
USGrph                 
  
 
                 
      
      |
173 | 113, 140,
172 | 3anbi123d 1338 |
. . . 4
           
USGrph              
                 

 
        
                 

 
        
                 
 
     
  
      
         
     
           
     
         |
174 | | prcom 4049 |
. . . . . . . . . . 11
    
  |
175 | 174 | eleq1i 2519 |
. . . . . . . . . 10
   
     |
176 | 175 | anbi2i 699 |
. . . . . . . . 9
    
   
  
  
    |
177 | 176 | anbi2i 699 |
. . . . . . . 8
     
  
      
          
      
     |
178 | | anandir 837 |
. . . . . . . 8
     
  
           
     
       |
179 | 177, 178 | bitr4i 256 |
. . . . . . 7
     
  
      
          
       |
180 | | prcom 4049 |
. . . . . . . . . . 11
    
  |
181 | 180 | eleq1i 2519 |
. . . . . . . . . 10
   
     |
182 | 181 | anbi2i 699 |
. . . . . . . . 9
    
   
  
  
    |
183 | 182 | anbi2i 699 |
. . . . . . . 8
     
  
      
          
      
     |
184 | | anandir 837 |
. . . . . . . 8
     
  
           
     
       |
185 | 183, 184 | bitr4i 256 |
. . . . . . 7
     
  
      
          
       |
186 | | prcom 4049 |
. . . . . . . . . . 11
    
  |
187 | 186 | eleq1i 2519 |
. . . . . . . . . 10
   
     |
188 | 187 | anbi2i 699 |
. . . . . . . . 9
    
   
  
  
    |
189 | 188 | anbi2i 699 |
. . . . . . . 8
     
  
      
          
      
     |
190 | | anandir 837 |
. . . . . . . 8
     
  
           
     
       |
191 | 189, 190 | bitr4i 256 |
. . . . . . 7
     
  
      
          
       |
192 | 179, 185,
191 | 3anbi123i 1196 |
. . . . . 6
         
      
         
     
           
     
           
               
         
           |
193 | | df-3an 986 |
. . . . . . . 8
    
    
 
      
        |
194 | | 3anrot 989 |
. . . . . . . . 9
    
    
 
  
  
  
    |
195 | | prcom 4049 |
. . . . . . . . . . 11
    
  |
196 | 195 | eleq1i 2519 |
. . . . . . . . . 10
   
     |
197 | | prcom 4049 |
. . . . . . . . . . 11
    
  |
198 | 197 | eleq1i 2519 |
. . . . . . . . . 10
   
     |
199 | | biid 240 |
. . . . . . . . . 10
   
     |
200 | 196, 198,
199 | 3anbi123i 1196 |
. . . . . . . . 9
    
    
 
  
  
  
    |
201 | 194, 200 | bitri 253 |
. . . . . . . 8
    
    
 
  
  
  
    |
202 | 193, 201 | bitr3i 255 |
. . . . . . 7
     
  
           
  
   |
203 | | df-3an 986 |
. . . . . . . 8
    
    
 
      
        |
204 | | biid 240 |
. . . . . . . . 9
   
     |
205 | | prcom 4049 |
. . . . . . . . . 10
    
  |
206 | 205 | eleq1i 2519 |
. . . . . . . . 9
   
     |
207 | 204, 198,
206 | 3anbi123i 1196 |
. . . . . . . 8
    
    
 
  
  
  
    |
208 | 203, 207 | bitr3i 255 |
. . . . . . 7
     
  
           
  
   |
209 | | df-3an 986 |
. . . . . . . 8
    
    
 
      
        |
210 | | 3anrot 989 |
. . . . . . . . 9
    
    
 
  
  
  
    |
211 | | 3anrot 989 |
. . . . . . . . 9
    
    
 
  
  
  
    |
212 | | biid 240 |
. . . . . . . . . 10
   
     |
213 | 196, 212,
206 | 3anbi123i 1196 |
. . . . . . . . 9
    
    
 
  
  
  
    |
214 | 210, 211,
213 | 3bitri 275 |
. . . . . . . 8
    
    
 
  
  
  
    |
215 | 209, 214 | bitr3i 255 |
. . . . . . 7
     
  
           
  
   |
216 | 202, 208,
215 | 3anbi123i 1196 |
. . . . . 6
         
         
               
     
      
  
     
    
     
    
     |
217 | | df-3an 986 |
. . . . . . 7
     
  
  
      
  
     
    
          
  
     
    
         
  
    |
218 | | anabs1 816 |
. . . . . . 7
         
  
      
  
         
  
 
      
  
     
    
     |
219 | | anidm 649 |
. . . . . . 7
     
  
  
      
  
      
  
  
   |
220 | 217, 218,
219 | 3bitri 275 |
. . . . . 6
     
  
  
      
  
     
    
      
  
  
   |
221 | 192, 216,
220 | 3bitri 275 |
. . . . 5
         
      
         
     
           
     
            
  
   |
222 | 221 | a1i 11 |
. . . 4
           
USGrph        
       
           
     
           
     
            
  
    |
223 | 173, 222 | bitrd 257 |
. . 3
           
USGrph              
                 

 
        
                 

 
        
                 
 
  
  
  
     |
224 | 7, 95, 223 | 3bitrd 283 |
. 2
           
USGrph     
 FriendGrph    
  
  
    |
225 | 224 | ex 436 |
1
  


      
USGrph     
FriendGrph
  
  
  
      |