Step | Hyp | Ref
| Expression |
1 | | efgval.r |
. 2
~FG    |
2 | | vex 3034 |
. . . . . . . . . . . 12
 |
3 | | 2on 7208 |
. . . . . . . . . . . . 13
 |
4 | 3 | elexi 3041 |
. . . . . . . . . . . 12
 |
5 | 2, 4 | xpex 6614 |
. . . . . . . . . . 11
   |
6 | | wrdexg 12729 |
. . . . . . . . . . 11
   Word     |
7 | | fvi 5937 |
. . . . . . . . . . 11
Word   Word    Word     |
8 | 5, 6, 7 | mp2b 10 |
. . . . . . . . . 10
Word    Word    |
9 | | xpeq1 4853 |
. . . . . . . . . . . 12
       |
10 | | wrdeq 12740 |
. . . . . . . . . . . 12
    
Word   Word     |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
 Word   Word     |
12 | 11 | fveq2d 5883 |
. . . . . . . . . 10
 Word    Word      |
13 | 8, 12 | syl5eqr 2519 |
. . . . . . . . 9
 Word   Word      |
14 | | efgval.w |
. . . . . . . . 9
Word     |
15 | 13, 14 | syl6eqr 2523 |
. . . . . . . 8
 Word     |
16 | | ereq2 7389 |
. . . . . . . 8
Word    Word
 
   |
17 | 15, 16 | syl 17 |
. . . . . . 7
  Word
 
   |
18 | | raleq 2973 |
. . . . . . . . 9
  

   splice                    
   splice                      |
19 | 18 | ralbidv 2829 |
. . . . . . . 8
  
         
    splice                             

   splice                      |
20 | 15, 19 | raleqbidv 2987 |
. . . . . . 7
  
Word    
         
    splice                    
         
    splice                      |
21 | 17, 20 | anbi12d 725 |
. . . . . 6
   Word    Word              

   splice                   


           
   splice                       |
22 | 21 | abbidv 2589 |
. . . . 5
   Word    Word              

   splice                        
         
    splice                       |
23 | 22 | inteqd 4231 |
. . . 4
    Word    Word              

   splice                         
         
    splice                       |
24 | | df-efg 17437 |
. . . 4
~FG
    Word    Word              

   splice                       |
25 | 14 | efglem 17444 |
. . . . 5
    
         
    splice                     |
26 | | intexab 4559 |
. . . . 5
    
           
   splice                        
         
    splice                       |
27 | 25, 26 | mpbi 213 |
. . . 4
   
           
   splice                      |
28 | 23, 24, 27 | fvmpt 5963 |
. . 3
 ~FG      
           
   splice                       |
29 | | fvprc 5873 |
. . . 4
 ~FG     |
30 | | abn0 3754 |
. . . . . . . 8
   

         
    splice                        
           
   splice                      |
31 | 25, 30 | mpbir 214 |
. . . . . . 7
  
           
   splice                      |
32 | | intssuni 4248 |
. . . . . . 7
   

         
    splice                         
         
    splice                         
         
    splice                       |
33 | 31, 32 | ax-mp 5 |
. . . . . 6
   
           
   splice                        

         
    splice                      |
34 | | erssxp 7404 |
. . . . . . . . . . . 12
     |
35 | 14 | efgrcl 17443 |
. . . . . . . . . . . . . . . . . 18
 
Word      |
36 | 35 | simpld 466 |
. . . . . . . . . . . . . . . . 17
   |
37 | 36 | con3i 142 |
. . . . . . . . . . . . . . . 16
   |
38 | 37 | eq0rdv 3773 |
. . . . . . . . . . . . . . 15
   |
39 | 38 | xpeq2d 4863 |
. . . . . . . . . . . . . 14
       |
40 | | xp0 5261 |
. . . . . . . . . . . . . 14
   |
41 | 39, 40 | syl6eq 2521 |
. . . . . . . . . . . . 13
     |
42 | | ss0b 3767 |
. . . . . . . . . . . . 13
       |
43 | 41, 42 | sylibr 217 |
. . . . . . . . . . . 12
     |
44 | 34, 43 | sylan9ssr 3432 |
. . . . . . . . . . 11
     |
45 | 44 | ex 441 |
. . . . . . . . . 10
 
   |
46 | 45 | adantrd 475 |
. . . . . . . . 9
    
         
    splice                       |
47 | 46 | alrimiv 1781 |
. . . . . . . 8
     

         
    splice                       |
48 | | sseq1 3439 |
. . . . . . . . 9
 
   |
49 | 48 | ralab2 3191 |
. . . . . . . 8
 
  
           
   splice                          

         
    splice                       |
50 | 47, 49 | sylibr 217 |
. . . . . . 7
    
           
   splice                        |
51 | | unissb 4221 |
. . . . . . 7
     
         
    splice                        
           
   splice                        |
52 | 50, 51 | sylibr 217 |
. . . . . 6
     
         
    splice                       |
53 | 33, 52 | syl5ss 3429 |
. . . . 5
     
         
    splice                       |
54 | | ss0 3768 |
. . . . 5
    

         
    splice                         
         
    splice                       |
55 | 53, 54 | syl 17 |
. . . 4
     
         
    splice                       |
56 | 29, 55 | eqtr4d 2508 |
. . 3
 ~FG      

         
    splice                       |
57 | 28, 56 | pm2.61i 169 |
. 2
~FG      
           
   splice                      |
58 | 1, 57 | eqtri 2493 |
1
    
         
    splice                      |