Step | Hyp | Ref
| Expression |
1 | | sikexlem.1 |
. . 3
1c k 1c |
2 | | sikexlem.2 |
. . 3
1c k 1c |
3 | | ssofeq 4078 |
. . 3
 
1c
k
1c
1c k 1c  
1c k
1c      |
4 | 1, 2, 3 | mp2an 653 |
. 2
  1c k 1c 
   |
5 | | df-ral 2620 |
. . 3
 
1c
k
1c      1c k 1c 
    |
6 | | elxpk 4197 |
. . . . . . . 8
 1c k 1c          1c
1c   |
7 | | el1c 4140 |
. . . . . . . . . . . . . 14
 1c 
    |
8 | | el1c 4140 |
. . . . . . . . . . . . . 14
 1c 
    |
9 | 7, 8 | anbi12i 678 |
. . . . . . . . . . . . 13
 
1c 1c  
  
     |
10 | | eeanv 1913 |
. . . . . . . . . . . . 13
       
    
  
     |
11 | 9, 10 | bitr4i 243 |
. . . . . . . . . . . 12
 
1c 1c             |
12 | 11 | anbi2i 675 |
. . . . . . . . . . 11
      1c
1c                  |
13 | | df-3an 936 |
. . . . . . . . . . . . . 14
                
      |
14 | | ancom 437 |
. . . . . . . . . . . . . 14
       
                 |
15 | 13, 14 | bitri 240 |
. . . . . . . . . . . . 13
              
        |
16 | 15 | 2exbii 1583 |
. . . . . . . . . . . 12
       
          
     
      |
17 | | 19.42vv 1907 |
. . . . . . . . . . . 12
                          
      |
18 | 16, 17 | bitri 240 |
. . . . . . . . . . 11
       
                
      |
19 | 12, 18 | bitr4i 243 |
. . . . . . . . . 10
      1c
1c         
      |
20 | 19 | 2exbii 1583 |
. . . . . . . . 9
          1c
1c                    |
21 | | exrot4 1745 |
. . . . . . . . 9
             
                       |
22 | 20, 21 | bitr4i 243 |
. . . . . . . 8
          1c
1c                    |
23 | | snex 4112 |
. . . . . . . . . 10
 
 |
24 | | snex 4112 |
. . . . . . . . . 10
 
 |
25 | | opkeq1 4060 |
. . . . . . . . . . 11
             |
26 | 25 | eqeq2d 2364 |
. . . . . . . . . 10
               |
27 | | opkeq2 4061 |
. . . . . . . . . . 11
           
     |
28 | 27 | eqeq2d 2364 |
. . . . . . . . . 10
            
      |
29 | 23, 24, 26, 28 | ceqsex2v 2897 |
. . . . . . . . 9
       
         
     |
30 | 29 | 2exbii 1583 |
. . . . . . . 8
             
      
         |
31 | 6, 22, 30 | 3bitri 262 |
. . . . . . 7
 1c k 1c             |
32 | 31 | imbi1i 315 |
. . . . . 6
  1c k
1c

             
    |
33 | | 19.23vv 1892 |
. . . . . 6
             
     
   
        |
34 | 32, 33 | bitr4i 243 |
. . . . 5
  1c k
1c

              
    |
35 | 34 | albii 1566 |
. . . 4
    1c k 1c 
               

    |
36 | | alrot3 1738 |
. . . 4
       
   
                
        |
37 | 35, 36 | bitri 240 |
. . 3
    1c k 1c 
               

    |
38 | | opkex 4114 |
. . . . 5
   
    |
39 | | eleq1 2413 |
. . . . . 6
        
          |
40 | | eleq1 2413 |
. . . . . 6
        
          |
41 | 39, 40 | bibi12d 312 |
. . . . 5
         
                    |
42 | 38, 41 | ceqsalv 2886 |
. . . 4
          

         
          |
43 | 42 | 2albii 1567 |
. . 3
       
   
              
      
      |
44 | 5, 37, 43 | 3bitri 262 |
. 2
 
1c
k
1c                         |
45 | 4, 44 | bitri 240 |
1
         
      
      |