Step | Hyp | Ref
| Expression |
1 | | ne0i 3728 |
. . 3
   ClWWalksN    
  ClWWalksN       |
2 | | ndmfv 5903 |
. . . 4
  ClWWalksN   
ClWWalksN       |
3 | 2 | necon1ai 2670 |
. . 3
   ClWWalksN
     ClWWalksN    |
4 | | oveq12 6317 |
. . . . . . . . . . 11
 
  ClWWalks   ClWWalks    |
5 | | rabeq 3024 |
. . . . . . . . . . 11
  ClWWalks   ClWWalks
   ClWWalks         ClWWalks         |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
 
   ClWWalks         ClWWalks         |
7 | 6 | mpteq2dv 4483 |
. . . . . . . . 9
 
  
 ClWWalks         
 ClWWalks          |
8 | | df-clwwlkn 25559 |
. . . . . . . . 9
ClWWalksN      ClWWalks          |
9 | | nn0ex 10899 |
. . . . . . . . . 10
 |
10 | 9 | mptex 6152 |
. . . . . . . . 9

  ClWWalks
        |
11 | 7, 8, 10 | ovmpt2a 6446 |
. . . . . . . 8
 
  ClWWalksN
    ClWWalks
         |
12 | 11 | 3adant3 1050 |
. . . . . . 7
 

  
ClWWalksN   
 ClWWalks          |
13 | 12 | dmeqd 5042 |
. . . . . 6
 

   ClWWalksN
    ClWWalks
         |
14 | 13 | eleq2d 2534 |
. . . . 5
 

   
ClWWalksN 
 
 ClWWalks           |
15 | | dmopabss 5052 |
. . . . . . . 8
    

 ClWWalks          |
16 | 15 | sseli 3414 |
. . . . . . 7
     
  ClWWalks
          |
17 | | clwwlkn 25574 |
. . . . . . . . . . . . . . . 16
 
  
ClWWalksN       ClWWalks         |
18 | 17 | 3expa 1231 |
. . . . . . . . . . . . . . 15
   
   ClWWalksN       ClWWalks
        |
19 | 18 | eleq2d 2534 |
. . . . . . . . . . . . . 14
   
    ClWWalksN    
  ClWWalks          |
20 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . 21
           |
21 | 20 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . . . . 20
     
       |
22 | 21 | elrab 3184 |
. . . . . . . . . . . . . . . . . . 19
   ClWWalks
        ClWWalks         |
23 | | clwwlkprop 25577 |
. . . . . . . . . . . . . . . . . . . 20
  ClWWalks  
Word    |
24 | | simpl3 1035 |
. . . . . . . . . . . . . . . . . . . . 21
  
Word       Word   |
25 | | lencl 12737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 Word       |
26 | | eleq1 2537 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
    
   |
27 | 25, 26 | syl5ibcom 228 |
. . . . . . . . . . . . . . . . . . . . . . 23
 Word         |
28 | 27 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . . . . . . . . 22
 
Word          |
29 | 28 | impac 633 |
. . . . . . . . . . . . . . . . . . . . 21
  
Word       
       |
30 | 24, 29 | jca 541 |
. . . . . . . . . . . . . . . . . . . 20
  
Word        Word 
        |
31 | 23, 30 | sylan 479 |
. . . . . . . . . . . . . . . . . . 19
   ClWWalks       
Word 
        |
32 | 22, 31 | sylbi 200 |
. . . . . . . . . . . . . . . . . 18
   ClWWalks
       Word          |
33 | 32 | anim2i 579 |
. . . . . . . . . . . . . . . . 17
   
  ClWWalks
      
 
 
Word 
         |
34 | | 3anass 1011 |
. . . . . . . . . . . . . . . . 17
   
Word 
         
Word 
         |
35 | 33, 34 | sylibr 217 |
. . . . . . . . . . . . . . . 16
   
  ClWWalks
      
 
 Word 
        |
36 | 35 | ex 441 |
. . . . . . . . . . . . . . 15
 
    ClWWalks         
Word 
         |
37 | 36 | adantr 472 |
. . . . . . . . . . . . . 14
   
    ClWWalks         
Word 
         |
38 | 19, 37 | sylbid 223 |
. . . . . . . . . . . . 13
   
    ClWWalksN      

Word 
         |
39 | 38 | ex 441 |
. . . . . . . . . . . 12
 
     ClWWalksN
      
Word 
          |
40 | 39 | com23 80 |
. . . . . . . . . . 11
 
    ClWWalksN
    
  
Word 
          |
41 | 40 | a1d 25 |
. . . . . . . . . 10
 
    ClWWalksN     
  ClWWalksN    

 
 Word 
           |
42 | 8 | mpt2ndm0 6529 |
. . . . . . . . . . 11
    ClWWalksN
   |
43 | | fveq1 5878 |
. . . . . . . . . . . 12
  ClWWalksN    ClWWalksN           |
44 | | 0fv 5912 |
. . . . . . . . . . . 12
     |
45 | 43, 44 | syl6eq 2521 |
. . . . . . . . . . 11
  ClWWalksN    ClWWalksN       |
46 | | eqneqall 2654 |
. . . . . . . . . . 11
   ClWWalksN
       ClWWalksN     
  ClWWalksN    

 
 Word 
           |
47 | 42, 45, 46 | 3syl 18 |
. . . . . . . . . 10
      ClWWalksN     
  ClWWalksN    

 
 Word 
           |
48 | 41, 47 | pm2.61i 169 |
. . . . . . . . 9
   ClWWalksN
    
  ClWWalksN    

 
 Word 
          |
49 | 1, 48 | syl 17 |
. . . . . . . 8
   ClWWalksN    
   ClWWalksN       

Word 
          |
50 | 49 | pm2.43i 48 |
. . . . . . 7
   ClWWalksN    

 
 Word 
         |
51 | 16, 50 | syl5com 30 |
. . . . . 6
     
  ClWWalks
        
  ClWWalksN    
 
 Word 
         |
52 | | df-mpt 4456 |
. . . . . . 7

  ClWWalks
           
  ClWWalks
         |
53 | 52 | dmeqi 5041 |
. . . . . 6
   ClWWalks
           

 ClWWalks          |
54 | 51, 53 | eleq2s 2567 |
. . . . 5
 
  ClWWalks
      
   ClWWalksN      

Word 
         |
55 | 14, 54 | syl6bi 236 |
. . . 4
 

   
ClWWalksN     ClWWalksN
      
Word 
          |
56 | | 3ianor 1024 |
. . . . 5
  
   
    |
57 | | df-3or 1008 |
. . . . . 6
  
 
 


    |
58 | | ianor 496 |
. . . . . . . 8
       |
59 | 42 | dmeqd 5042 |
. . . . . . . . . . 11
    ClWWalksN    |
60 | 59 | eleq2d 2534 |
. . . . . . . . . 10
    
ClWWalksN 
   |
61 | | dm0 5054 |
. . . . . . . . . . 11
 |
62 | 61 | eleq2i 2541 |
. . . . . . . . . 10

  |
63 | 60, 62 | syl6bb 269 |
. . . . . . . . 9
    
ClWWalksN 
   |
64 | | noel 3726 |
. . . . . . . . . 10
 |
65 | 64 | pm2.21i 136 |
. . . . . . . . 9

   ClWWalksN      

Word 
         |
66 | 63, 65 | syl6bi 236 |
. . . . . . . 8
    
ClWWalksN     ClWWalksN
      
Word 
          |
67 | 58, 66 | sylbir 218 |
. . . . . . 7
     ClWWalksN     ClWWalksN      

Word 
          |
68 | 67, 66 | jaoi 386 |
. . . . . 6
  
 
 
  ClWWalksN     ClWWalksN      

Word 
          |
69 | 57, 68 | sylbi 200 |
. . . . 5
  
  
 ClWWalksN  
  ClWWalksN    
 
 Word 
          |
70 | 56, 69 | sylbi 200 |
. . . 4
  
 
  ClWWalksN     ClWWalksN      

Word 
          |
71 | 55, 70 | pm2.61i 169 |
. . 3
  ClWWalksN  
  ClWWalksN    
 
 Word 
         |
72 | 1, 3, 71 | 3syl 18 |
. 2
   ClWWalksN    
   ClWWalksN      

Word 
         |
73 | 72 | pm2.43i 48 |
1
   ClWWalksN    
 
 Word 
        |