Step | Hyp | Ref
| Expression |
1 | | cusisusgra 25265 |
. . 3
 ComplUSGrph USGrph
  |
2 | | cusgrares.f |
. . . 4
         |
3 | 2 | usgrares1 25217 |
. . 3
  USGrph
     USGrph   |
4 | 1, 3 | sylan 479 |
. 2
  ComplUSGrph      USGrph   |
5 | | iscusgra0 25264 |
. . . 4
 ComplUSGrph  USGrph  
           |
6 | | usgraf1o 25164 |
. . . . . . . . . . . . . . . . . . . . . 22
 USGrph       |
7 | | f1ocnvdm 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         
          |
8 | 7 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                            |
9 | | elpri 3976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
    
   |
10 | | ssnid 3989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
   |
11 | | sneq 3969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
  
    |
12 | 10, 11 | syl5eleqr 2556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
     |
13 | 12 | notnotd 128 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36

    |
14 | | df-nel 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
       |
15 | 13, 14 | sylnibr 312 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     |
16 | | ssnid 3989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
   |
17 | | sneq 3969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
  
    |
18 | 16, 17 | syl5eleqr 2556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
     |
19 | 18 | notnotd 128 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36

    |
20 | | df-nel 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
       |
21 | 19, 20 | sylnibr 312 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
     |
22 | 15, 21 | orim12i 525 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
     |
23 | 9, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
 
     |
24 | | ianor 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
           |
25 | 23, 24 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
    
       |
26 | 25 | con2i 124 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
      
     |
27 | | df-nel 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
     |
28 | 26, 27 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
            |
29 | 28 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                       |
30 | | f1ocnvfv2 6194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         
                 |
31 | 30 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                   |
32 | | neleq2 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                            
      |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                              
      |
34 | 29, 33 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                |
35 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                           |
36 | | neleq2 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                
    
               |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
             
               |
38 | 37 | elrab 3184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         
    
                        |
39 | 8, 34, 38 | sylanbrc 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                          
       |
40 | 39, 31 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                           
                       |
41 | 40 | exp31 615 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                         
                         |
42 | 41 | com23 80 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               
         
                         |
43 | 42 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
        
         
                          |
44 | 43 | com14 90 |
. . . . . . . . . . . . . . . . . . . . . 22
       
      
         
                          |
45 | 6, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
 USGrph          
         
                          |
46 | 45 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . 20
   USGrph


         
         
                          |
47 | 46 | imp 436 |
. . . . . . . . . . . . . . . . . . 19
    USGrph

       
            
                         |
48 | 47 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
     USGrph 
                         
                         |
49 | 48 | imp31 439 |
. . . . . . . . . . . . . . . . 17
       USGrph


  
                     
                       |
50 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
                           |
51 | 50 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . 18
                
                  |
52 | 51 | rspcev 3136 |
. . . . . . . . . . . . . . . . 17
          
                      
              |
53 | 49, 52 | syl 17 |
. . . . . . . . . . . . . . . 16
       USGrph


  
             
              |
54 | | usgrafun 25155 |
. . . . . . . . . . . . . . . . . . 19
 USGrph
  |
55 | | funfn 5618 |
. . . . . . . . . . . . . . . . . . 19

  |
56 | 54, 55 | sylib 201 |
. . . . . . . . . . . . . . . . . 18
 USGrph   |
57 | 56 | ad6antr 750 |
. . . . . . . . . . . . . . . . 17
       USGrph


  
              |
58 | | ssrab2 3500 |
. . . . . . . . . . . . . . . . 17
       |
59 | | fvelimab 5936 |
. . . . . . . . . . . . . . . . 17
                      
                 |
60 | 57, 58, 59 | sylancl 675 |
. . . . . . . . . . . . . . . 16
       USGrph


  
                         
                 |
61 | 53, 60 | mpbird 240 |
. . . . . . . . . . . . . . 15
       USGrph


  
                           |
62 | 2 | rneqi 5067 |
. . . . . . . . . . . . . . . 16
 
       |
63 | | df-ima 4852 |
. . . . . . . . . . . . . . . 16
   
       
       |
64 | 62, 63 | eqtr4i 2496 |
. . . . . . . . . . . . . . 15
   
       |
65 | 61, 64 | syl6eleqr 2560 |
. . . . . . . . . . . . . 14
       USGrph


  
                 |
66 | 65 | exp31 615 |
. . . . . . . . . . . . 13
     USGrph 
                       |
67 | 66 | ralimdva 2805 |
. . . . . . . . . . . 12
    USGrph

              
               |
68 | 67 | imp 436 |
. . . . . . . . . . 11
     USGrph 
                             |
69 | | raldifb 3562 |
. . . . . . . . . . 11
 
       
   
               |
70 | 68, 69 | sylib 201 |
. . . . . . . . . 10
     USGrph 
                             |
71 | | dif32 3697 |
. . . . . . . . . . 11
                 |
72 | 71 | raleqi 2977 |
. . . . . . . . . 10
 
    
                      |
73 | 70, 72 | sylibr 217 |
. . . . . . . . 9
     USGrph 
                             |
74 | 73 | exp31 615 |
. . . . . . . 8
   USGrph


            
                 |
75 | 74 | com23 80 |
. . . . . . 7
   USGrph


 
          
                 |
76 | 75 | ralimdva 2805 |
. . . . . 6
  USGrph
  

           
                 |
77 | 76 | impancom 447 |
. . . . 5
  USGrph

          

                    |
78 | | raldifb 3562 |
. . . . 5
 

                
                    |
79 | 77, 78 | syl6ib 234 |
. . . 4
  USGrph

          
                      |
80 | 5, 79 | syl 17 |
. . 3
 ComplUSGrph 
                      |
81 | 80 | imp 436 |
. 2
  ComplUSGrph                       |
82 | | usgrav 25144 |
. . . 4
 USGrph 
   |
83 | | difexg 4545 |
. . . . 5
       |
84 | | resexg 5153 |
. . . . . 6
  
        |
85 | 2, 84 | syl5eqel 2553 |
. . . . 5
   |
86 | | iscusgra 25263 |
. . . . 5
            ComplUSGrph
     USGrph
                       |
87 | 83, 85, 86 | syl2an 485 |
. . . 4
 
      ComplUSGrph
     USGrph
                       |
88 | 1, 82, 87 | 3syl 18 |
. . 3
 ComplUSGrph      ComplUSGrph      USGrph
                       |
89 | 88 | adantr 472 |
. 2
  ComplUSGrph       ComplUSGrph
     USGrph
                       |
90 | 4, 81, 89 | mpbir2and 936 |
1
  ComplUSGrph      ComplUSGrph   |