Step | Hyp | Ref
| Expression |
1 | | fusgraimpcl 40012 |
. 2
 FinUSGrph  USGrph
GrOrder      |
2 | | relusgra 25111 |
. . . . . . . . . . 11
USGrph |
3 | | 1st2nd 6866 |
. . . . . . . . . . 11
  USGrph USGrph              |
4 | 2, 3 | mpan 681 |
. . . . . . . . . 10
 USGrph              |
5 | | eleq1 2528 |
. . . . . . . . . . . 12
            
USGrph            USGrph   |
6 | | df-br 4417 |
. . . . . . . . . . . 12
     USGrph                USGrph  |
7 | 5, 6 | syl6bbr 271 |
. . . . . . . . . . 11
            
USGrph     USGrph        |
8 | | mptresid 5178 |
. . . . . . . . . . . . . 14
  Edges         Edges     
   |
9 | | fvex 5898 |
. . . . . . . . . . . . . . 15
Edges       |
10 | 9 | mptrabex 6162 |
. . . . . . . . . . . . . 14
  Edges         |
11 | 8, 10 | eqeltrri 2537 |
. . . . . . . . . . . . 13
 Edges     
   |
12 | | eleq1 2528 |
. . . . . . . . . . . . . 14
    
        |
13 | 12 | adantl 472 |
. . . . . . . . . . . . 13
           
       |
14 | | eleq1 2528 |
. . . . . . . . . . . . . 14
 
   |
15 | 14 | adantl 472 |
. . . . . . . . . . . . 13
 
     |
16 | | df-br 4417 |
. . . . . . . . . . . . . 14
 USGrph    USGrph  |
17 | | opex 4678 |
. . . . . . . . . . . . . . . . 17
    |
18 | | vtxvalaltv 39968 |
. . . . . . . . . . . . . . . . 17
   
VtxALTV               |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
VtxALTV              |
20 | | vex 3060 |
. . . . . . . . . . . . . . . . 17
 |
21 | | vex 3060 |
. . . . . . . . . . . . . . . . 17
 |
22 | 20, 21 | op1st 6828 |
. . . . . . . . . . . . . . . 16
      
 |
23 | 19, 22 | eqtr2i 2485 |
. . . . . . . . . . . . . . 15
VtxALTV       |
24 | | eqid 2462 |
. . . . . . . . . . . . . . 15
Edges     
Edges       |
25 | | eqid 2462 |
. . . . . . . . . . . . . . 15

Edges     


Edges     
  |
26 | 23, 24, 25 | usgresvm1 40028 |
. . . . . . . . . . . . . 14
     USGrph 
    USGrph 
Edges     
    |
27 | 16, 26 | sylanb 479 |
. . . . . . . . . . . . 13
  USGrph  
  
USGrph 
Edges     
    |
28 | | eleq1 2528 |
. . . . . . . . . . . . . 14
 
Edges     
  
 Edges     
     |
29 | 28 | adantl 472 |
. . . . . . . . . . . . 13
     

Edges     
     Edges           |
30 | | usgrafisbaseALT 40025 |
. . . . . . . . . . . . 13
  USGrph        |
31 | | residfi 39081 |
. . . . . . . . . . . . . . . 16


Edges     
   Edges     

  |
32 | | simpr1 1020 |
. . . . . . . . . . . . . . . . . . . . 21
    
USGrph         USGrph   |
33 | | eleq1 2528 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
  
       |
34 | 33 | eqcoms 2470 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
       |
35 | | hashclb 12572 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
       |
36 | 35 | bicomd 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
   |
37 | 20, 36 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
38 | 37 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
  |
39 | 34, 38 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
40 | 39 | 3ad2ant2 1036 |
. . . . . . . . . . . . . . . . . . . . . 22
  USGrph              |
41 | 40 | impcom 436 |
. . . . . . . . . . . . . . . . . . . . 21
    
USGrph           |
42 | 32, 41 | jca 539 |
. . . . . . . . . . . . . . . . . . . 20
    
USGrph          USGrph
   |
43 | | usgrav 25114 |
. . . . . . . . . . . . . . . . . . . . . . 23
 USGrph
    |
44 | | df-br 4417 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 FinUSGrph    FinUSGrph  |
45 | | isfusgra0 40010 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
  FinUSGrph
 USGrph     |
46 | 44, 45 | syl5bbr 267 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     FinUSGrph  USGrph
    |
47 | 43, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
 USGrph
    FinUSGrph
 USGrph     |
48 | 47 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . . . . 21
  USGrph            FinUSGrph  USGrph     |
49 | 48 | adantl 472 |
. . . . . . . . . . . . . . . . . . . 20
    
USGrph             FinUSGrph  USGrph
    |
50 | 42, 49 | mpbird 240 |
. . . . . . . . . . . . . . . . . . 19
    
USGrph            FinUSGrph  |
51 | 17, 18 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 USGrph
VtxALTV               |
52 | 51, 22 | syl6req 2513 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 USGrph
VtxALTV        |
53 | 52 | eleq2d 2525 |
. . . . . . . . . . . . . . . . . . . . . . 23
 USGrph

VtxALTV         |
54 | 53 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . . 22
 USGrph

VtxALTV         |
55 | 54 | a1d 26 |
. . . . . . . . . . . . . . . . . . . . 21
 USGrph
      

VtxALTV          |
56 | 55 | 3imp 1208 |
. . . . . . . . . . . . . . . . . . . 20
  USGrph       
VtxALTV        |
57 | 56 | adantl 472 |
. . . . . . . . . . . . . . . . . . 19
    
USGrph        
VtxALTV        |
58 | 50, 57 | jca 539 |
. . . . . . . . . . . . . . . . . 18
    
USGrph             FinUSGrph VtxALTV         |
59 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . 19
VtxALTV     
VtxALTV       |
60 | | df-ov 6318 |
. . . . . . . . . . . . . . . . . . 19
 Edges  Edges       |
61 | 60 | eqcomi 2471 |
. . . . . . . . . . . . . . . . . . . 20
Edges       Edges   |
62 | | rabeq 3050 |
. . . . . . . . . . . . . . . . . . . 20
 Edges     
 Edges  
Edges      
  Edges     |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19

Edges     

  Edges    |
64 | 59, 60, 63 | usgfislem2 40030 |
. . . . . . . . . . . . . . . . . 18
     FinUSGrph VtxALTV         Edges 

Edges     

   |
65 | 58, 64 | syl 17 |
. . . . . . . . . . . . . . . . 17
    
USGrph           Edges 

Edges     

   |
66 | 65 | biimprd 231 |
. . . . . . . . . . . . . . . 16
    
USGrph           Edges        Edges     |
67 | 31, 66 | syl5bi 225 |
. . . . . . . . . . . . . . 15
    
USGrph          
Edges     
   Edges     |
68 | 67 | imp 435 |
. . . . . . . . . . . . . 14
      USGrph        

Edges     
    Edges    |
69 | | usgedgffibi 40019 |
. . . . . . . . . . . . . . . . 17
 USGrph
  Edges     |
70 | 69 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . 16
  USGrph        
 Edges     |
71 | 70 | adantl 472 |
. . . . . . . . . . . . . . 15
    
USGrph           Edges     |
72 | 71 | adantr 471 |
. . . . . . . . . . . . . 14
      USGrph        

Edges     
     Edges     |
73 | 68, 72 | mpbird 240 |
. . . . . . . . . . . . 13
      USGrph        

Edges     
     |
74 | 2, 11, 13, 15, 27, 29, 30, 73 | brfi1ind 12685 |
. . . . . . . . . . . 12
      USGrph    
           |
75 | 74 | ex 440 |
. . . . . . . . . . 11
     USGrph    
            |
76 | 7, 75 | syl6bi 236 |
. . . . . . . . . 10
            
USGrph              |
77 | 4, 76 | mpcom 37 |
. . . . . . . . 9
 USGrph             |
78 | 77 | imp 435 |
. . . . . . . 8
  USGrph
           |
79 | | rnfi 7883 |
. . . . . . . 8
           |
80 | 78, 79 | syl 17 |
. . . . . . 7
  USGrph
           |
81 | | edgval 25115 |
. . . . . . . . 9
 USGrph Edges
        |
82 | 81 | eleq1d 2524 |
. . . . . . . 8
 USGrph  Edges  
       |
83 | 82 | adantr 471 |
. . . . . . 7
  USGrph
      Edges          |
84 | 80, 83 | mpbird 240 |
. . . . . 6
  USGrph
     Edges     |
85 | 84 | ex 440 |
. . . . 5
 USGrph      Edges      |
86 | 85 | a1dd 47 |
. . . 4
 USGrph       FinUSGrph Edges       |
87 | | gordval 39973 |
. . . . . 6
 USGrph GrOrder
            |
88 | 87 | eleq1d 2524 |
. . . . 5
 USGrph  GrOrder  
           |
89 | | fvex 5898 |
. . . . . 6
     |
90 | | hashclb 12572 |
. . . . . 6
         
           |
91 | 89, 90 | ax-mp 5 |
. . . . 5
    
          |
92 | 88, 91 | syl6bbr 271 |
. . . 4
 USGrph  GrOrder  
       |
93 | | usgsizedg 39980 |
. . . . . . 7
 USGrph GrSize
     Edges      |
94 | 93 | eleq1d 2524 |
. . . . . 6
 USGrph  GrSize  
   Edges       |
95 | | fvex 5898 |
. . . . . . 7
Edges    |
96 | | hashclb 12572 |
. . . . . . 7
 Edges    Edges  
   Edges       |
97 | 95, 96 | ax-mp 5 |
. . . . . 6
 Edges      Edges      |
98 | 94, 97 | syl6bbr 271 |
. . . . 5
 USGrph  GrSize  
Edges      |
99 | 98 | imbi2d 322 |
. . . 4
 USGrph   FinUSGrph GrSize
  
 FinUSGrph
Edges       |
100 | 86, 92, 99 | 3imtr4d 276 |
. . 3
 USGrph  GrOrder    FinUSGrph
GrSize       |
101 | 100 | imp 435 |
. 2
  USGrph
GrOrder     FinUSGrph GrSize      |
102 | 1, 101 | mpcom 37 |
1
 FinUSGrph GrSize
    |