Proof of Theorem usgra2wlkspthlem2
Step | Hyp | Ref
| Expression |
1 | | oveq2 6316 |
. . . . . . . . . . . . . 14
                   |
2 | 1 | feq2d 5725 |
. . . . . . . . . . . . 13
                 
           |
3 | | fz0tp 11918 |
. . . . . . . . . . . . . . 15
         |
4 | 3 | feq2i 5731 |
. . . . . . . . . . . . . 14
        
          |
5 | 4 | biimpi 199 |
. . . . . . . . . . . . 13
                   |
6 | 2, 5 | syl6bi 236 |
. . . . . . . . . . . 12
                             |
7 | 6 | ad2antll 743 |
. . . . . . . . . . 11
  USGrph

Word                   
           |
8 | 7 | adantr 472 |
. . . . . . . . . 10
   USGrph 
Word                      
 ..^                                                     |
9 | 8 | impcom 437 |
. . . . . . . . 9
                USGrph  Word                      
 ..^                                        |
10 | | eqeq12 2484 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
11 | 10 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . 20
                       |
12 | 11 | necon3d 2664 |
. . . . . . . . . . . . . . . . . . 19
                       |
13 | 12 | 3impia 1228 |
. . . . . . . . . . . . . . . . . 18
                     |
14 | 13 | adantr 472 |
. . . . . . . . . . . . . . . . 17
           
                                                   |
15 | 14 | adantl 473 |
. . . . . . . . . . . . . . . 16
    Word      USGrph 
                                                    
          |
16 | 15 | adantr 472 |
. . . . . . . . . . . . . . 15
     Word
     USGrph            
                                                             |
17 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . 21
    Word      USGrph 
                   
USGrph   |
18 | | usgrafun 25155 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 USGrph
  |
19 | | wrdf 12723 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 Word
   ..^      
  |
20 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      ..^      ..^   |
21 | 20 | feq2d 5725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         ..^      
   ..^      |
22 | | c0ex 9655 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
23 | 22 | prid1 4071 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    |
24 | | fzo0to2pr 12027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 ..^     |
25 | 23, 24 | eleqtrri 2548 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 ..^  |
26 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     ..^  
 ..^        |
27 | 25, 26 | mpan2 685 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    ..^  
      |
28 | 21, 27 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         ..^      
       |
29 | 19, 28 | mpan9 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  Word            |
30 | | fvelrn 6030 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
31 | 18, 29, 30 | syl2anr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
   Word      USGrph
           |
32 | 31 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
    Word      USGrph 
                   
          |
33 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                           |
34 | 33 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
    Word      USGrph 
                   
        
              |
35 | 32, 34 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . 21
    Word      USGrph 
                   
             |
36 | | usgraedgrn 25187 |
. . . . . . . . . . . . . . . . . . . . 21
  USGrph
                      |
37 | 17, 35, 36 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . 20
    Word      USGrph 
                   
          |
38 | 37 | ex 441 |
. . . . . . . . . . . . . . . . . . 19
   Word      USGrph
                                |
39 | | simplr 770 |
. . . . . . . . . . . . . . . . . . . . 21
    Word      USGrph 
                   
USGrph   |
40 | | 1ex 9656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
41 | 40 | prid2 4072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    |
42 | 41, 24 | eleqtrri 2548 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 ..^  |
43 | | ffvelrn 6035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     ..^  
 ..^        |
44 | 42, 43 | mpan2 685 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    ..^  
      |
45 | 21, 44 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         ..^      
       |
46 | 19, 45 | mpan9 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  Word            |
47 | | fvelrn 6030 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
48 | 18, 46, 47 | syl2anr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
   Word      USGrph
           |
49 | 48 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
    Word      USGrph 
                   
          |
50 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                           |
51 | 50 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
    Word      USGrph 
                   
        
              |
52 | 49, 51 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . 21
    Word      USGrph 
                   
             |
53 | | usgraedgrn 25187 |
. . . . . . . . . . . . . . . . . . . . 21
  USGrph
                      |
54 | 39, 52, 53 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . 20
    Word      USGrph 
                   
          |
55 | 54 | ex 441 |
. . . . . . . . . . . . . . . . . . 19
   Word      USGrph
                                |
56 | 38, 55 | anim12d 572 |
. . . . . . . . . . . . . . . . . 18
   Word      USGrph
                                                               |
57 | 56 | adantld 474 |
. . . . . . . . . . . . . . . . 17
   Word      USGrph
           
                                                  
            |
58 | 57 | imp 436 |
. . . . . . . . . . . . . . . 16
    Word      USGrph 
                                                    
        
           |
59 | 58 | adantr 472 |
. . . . . . . . . . . . . . 15
     Word
     USGrph            
                                                                       |
60 | | 3anan12 1020 |
. . . . . . . . . . . . . . 15
                          
        
        
            |
61 | 16, 59, 60 | sylanbrc 677 |
. . . . . . . . . . . . . 14
     Word
     USGrph            
                                                                               |
62 | 61 | exp41 621 |
. . . . . . . . . . . . 13
  Word       USGrph           
                                                                                  |
63 | 62 | impcom 437 |
. . . . . . . . . . . 12
  USGrph

Word                                                                                                   |
64 | | fveq2 5879 |
. . . . . . . . . . . . . . . . 17
                   |
65 | 64 | eqeq1d 2473 |
. . . . . . . . . . . . . . . 16
             
       |
66 | 65 | 3anbi2d 1370 |
. . . . . . . . . . . . . . 15
                   
    
   
    |
67 | 20, 24 | syl6eq 2521 |
. . . . . . . . . . . . . . . . 17
      ..^          |
68 | 67 | raleqdv 2979 |
. . . . . . . . . . . . . . . 16
      
 ..^                                                       |
69 | | 2wlklem 25373 |
. . . . . . . . . . . . . . . 16
 
                                                                  |
70 | 68, 69 | syl6bb 269 |
. . . . . . . . . . . . . . 15
      
 ..^                                                                      |
71 | 66, 70 | anbi12d 725 |
. . . . . . . . . . . . . 14
                    
  ..^                           
                                                       |
72 | 2 | imbi1d 324 |
. . . . . . . . . . . . . 14
                           
       
         
                                       |
73 | 71, 72 | imbi12d 327 |
. . . . . . . . . . . . 13
                     
  ..^                                                 
       
                     
                                                                                  |
74 | 73 | ad2antll 743 |
. . . . . . . . . . . 12
  USGrph

Word                          ..^                                                                                                                                                                  |
75 | 63, 74 | mpbird 240 |
. . . . . . . . . . 11
  USGrph

Word                       
 ..^                                                                       |
76 | 75 | imp 436 |
. . . . . . . . . 10
   USGrph 
Word                      
 ..^                                                  
       
            |
77 | 76 | impcom 437 |
. . . . . . . . 9
                USGrph  Word                      
 ..^                                      
       
           |
78 | | 2z 10993 |
. . . . . . . . . . . 12
 |
79 | 22, 40, 78 | 3pm3.2i 1208 |
. . . . . . . . . . 11
   |
80 | | 0ne1 10699 |
. . . . . . . . . . . 12
 |
81 | | 0ne2 10844 |
. . . . . . . . . . . 12
 |
82 | | 1ne2 10845 |
. . . . . . . . . . . 12
 |
83 | 80, 81, 82 | 3pm3.2i 1208 |
. . . . . . . . . . 11

  |
84 | 79, 83 | pm3.2i 462 |
. . . . . . . . . 10
 
     |
85 | | eqid 2471 |
. . . . . . . . . . 11
         |
86 | 85 | f13dfv 6191 |
. . . . . . . . . 10
  
 
                                                  |
87 | 84, 86 | mp1i 13 |
. . . . . . . . 9
                USGrph  Word                      
 ..^                                                                              |
88 | 9, 77, 87 | mpbir2and 936 |
. . . . . . . 8
                USGrph  Word                      
 ..^                                        |
89 | | df-f1 5594 |
. . . . . . . 8
                      |
90 | 88, 89 | sylib 201 |
. . . . . . 7
                USGrph  Word                      
 ..^                                           |
91 | 90 | simprd 470 |
. . . . . 6
                USGrph  Word                      
 ..^                             
   |
92 | 91 | expcom 442 |
. . . . 5
   USGrph 
Word                      
 ..^                                         
    |
93 | 92 | ex 441 |
. . . 4
  USGrph

Word                       
 ..^                                              |
94 | 93 | com23 80 |
. . 3
  USGrph

Word                   
                  ..^                                 |
95 | 94 | impancom 447 |
. 2
  USGrph
               Word                      
 ..^                                 |
96 | 95 | impcom 437 |
1
   Word       USGrph              
                  ..^                                |