Step | Hyp | Ref
| Expression |
1 | | ixpfi2.1 |
. . . 4
   |
2 | | inss2 3644 |
. . . 4
   |
3 | | ssfi 7810 |
. . . 4
  
      |
4 | 1, 2, 3 | sylancl 675 |
. . 3
     |
5 | | inss1 3643 |
. . . 4
   |
6 | | ixpfi2.2 |
. . . . 5
 
   |
7 | 6 | ralrimiva 2809 |
. . . 4
 
  |
8 | | ssralv 3479 |
. . . 4
    
       |
9 | 5, 7, 8 | mpsyl 64 |
. . 3
       |
10 | | ixpfi 7889 |
. . 3
               |
11 | 4, 9, 10 | syl2anc 673 |
. 2
       |
12 | | resixp 7575 |
. . . . 5
   
            |
13 | 5, 12 | mpan 684 |
. . . 4
   
        |
14 | 13 | a1i 11 |
. . 3
  
           |
15 | | simprl 772 |
. . . . . . . . . 10
 
  
     |
16 | | vex 3034 |
. . . . . . . . . . 11
 |
17 | 16 | elixp 7547 |
. . . . . . . . . 10
           |
18 | 15, 17 | sylib 201 |
. . . . . . . . 9
 
  
           |
19 | 18 | simprd 470 |
. . . . . . . 8
 
  
  
      |
20 | | simprr 774 |
. . . . . . . . . 10
 
  
     |
21 | | vex 3034 |
. . . . . . . . . . 11
 |
22 | 21 | elixp 7547 |
. . . . . . . . . 10
           |
23 | 20, 22 | sylib 201 |
. . . . . . . . 9
 
  
           |
24 | 23 | simprd 470 |
. . . . . . . 8
 
  
  
      |
25 | | r19.26 2904 |
. . . . . . . . 9
 
                        |
26 | | difss 3549 |
. . . . . . . . . . 11
   |
27 | | ssralv 3479 |
. . . . . . . . . . 11
    
                           |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . 10
 
                          |
29 | | ixpfi2.3 |
. . . . . . . . . . . . . . . 16
 

 
    |
30 | 29 | sseld 3417 |
. . . . . . . . . . . . . . 15
 

 
    
         |
31 | | elsni 3985 |
. . . . . . . . . . . . . . 15
             |
32 | 30, 31 | syl6 33 |
. . . . . . . . . . . . . 14
 

 
    
       |
33 | 29 | sseld 3417 |
. . . . . . . . . . . . . . 15
 

 
    
         |
34 | | elsni 3985 |
. . . . . . . . . . . . . . 15
             |
35 | 33, 34 | syl6 33 |
. . . . . . . . . . . . . 14
 

 
    
       |
36 | 32, 35 | anim12d 572 |
. . . . . . . . . . . . 13
 

 
                        |
37 | | eqtr3 2492 |
. . . . . . . . . . . . 13
                     |
38 | 36, 37 | syl6 33 |
. . . . . . . . . . . 12
 

 
                      |
39 | 38 | ralimdva 2805 |
. . . . . . . . . . 11
                               |
40 | 39 | adantr 472 |
. . . . . . . . . 10
 
  
   
                            |
41 | 28, 40 | syl5 32 |
. . . . . . . . 9
 
  
   
                         |
42 | 25, 41 | syl5bir 226 |
. . . . . . . 8
 
  
                              |
43 | 19, 24, 42 | mp2and 693 |
. . . . . . 7
 
  
                |
44 | 43 | biantrud 515 |
. . . . . 6
 
  
   
          
 
          
                |
45 | | fvres 5893 |
. . . . . . . 8
  
              |
46 | | fvres 5893 |
. . . . . . . 8
  
              |
47 | 45, 46 | eqeq12d 2486 |
. . . . . . 7
  
           
                |
48 | 47 | ralbiia 2822 |
. . . . . 6
 
    
             
              |
49 | | inundif 3836 |
. . . . . . . 8
       |
50 | 49 | raleqi 2977 |
. . . . . . 7
 
                          |
51 | | ralunb 3606 |
. . . . . . 7
 
                                           |
52 | 50, 51 | bitr3i 259 |
. . . . . 6
 
       
 
          
               |
53 | 44, 48, 52 | 3bitr4g 296 |
. . . . 5
 
  
   
             
     
           |
54 | 18 | simpld 466 |
. . . . . . 7
 
  
    |
55 | | fnssres 5699 |
. . . . . . 7
  
          |
56 | 54, 5, 55 | sylancl 675 |
. . . . . 6
 
  
          |
57 | 23 | simpld 466 |
. . . . . . 7
 
  
    |
58 | | fnssres 5699 |
. . . . . . 7
  
          |
59 | 57, 5, 58 | sylancl 675 |
. . . . . 6
 
  
          |
60 | | eqfnfv 5991 |
. . . . . 6
                    
  
             
         |
61 | 56, 59, 60 | syl2anc 673 |
. . . . 5
 
  
        
        
                |
62 | | eqfnfv 5991 |
. . . . . 6
 
  
           |
63 | 54, 57, 62 | syl2anc 673 |
. . . . 5
 
  
  

           |
64 | 53, 61, 63 | 3bitr4d 293 |
. . . 4
 
  
        
     |
65 | 64 | ex 441 |
. . 3
   


     
  
    |
66 | 14, 65 | dom2lem 7627 |
. 2
  
       
        |
67 | | f1fi 7879 |
. 2
       
       
          |
68 | 11, 66, 67 | syl2anc 673 |
1
 
  |