Step | Hyp | Ref
| Expression |
1 | | f2ndres 6835 |
. . . 4
                |
2 | | 1stmbfm.1 |
. . . . . 6
  sigAlgebra |
3 | | 1stmbfm.2 |
. . . . . 6
  sigAlgebra |
4 | | sxuni 29089 |
. . . . . 6
   sigAlgebra
 sigAlgebra      
×s    |
5 | 2, 3, 4 | syl2anc 673 |
. . . . 5
      
×s    |
6 | 5 | feq2d 5725 |
. . . 4
    
            
         ×s        |
7 | 1, 6 | mpbii 216 |
. . 3
   
      
×s       |
8 | | unielsiga 29024 |
. . . . 5
  sigAlgebra    |
9 | 3, 8 | syl 17 |
. . . 4
    |
10 | | sxsiga 29087 |
. . . . . 6
   sigAlgebra
 sigAlgebra 
×s   sigAlgebra |
11 | 2, 3, 10 | syl2anc 673 |
. . . . 5
 
×s   sigAlgebra |
12 | | unielsiga 29024 |
. . . . 5
  ×s   sigAlgebra   ×s   ×s    |
13 | 11, 12 | syl 17 |
. . . 4
   ×s   ×s    |
14 | 9, 13 | elmapd 7504 |
. . 3
    
      
×s  
          ×s        |
15 | 7, 14 | mpbird 240 |
. 2
   
      
×s     |
16 | | sgon 29020 |
. . . . . . . . . . 11
  sigAlgebra sigAlgebra     |
17 | | sigasspw 29012 |
. . . . . . . . . . 11
 sigAlgebra       |
18 | | pwssb 4361 |
. . . . . . . . . . . 12
  

   |
19 | 18 | biimpi 199 |
. . . . . . . . . . 11
   
   |
20 | 3, 16, 17, 19 | 4syl 19 |
. . . . . . . . . 10
     |
21 | 20 | r19.21bi 2776 |
. . . . . . . . 9
 
    |
22 | | xpss2 4949 |
. . . . . . . . 9
   

      |
23 | 21, 22 | syl 17 |
. . . . . . . 8
 
  

      |
24 | 23 | sseld 3417 |
. . . . . . 7
 
            |
25 | 24 | pm4.71rd 647 |
. . . . . 6
 
    
            |
26 | | ffn 5739 |
. . . . . . . 8
 
                          |
27 | | elpreima 6017 |
. . . . . . . 8
 
                    
      
            |
28 | 1, 26, 27 | mp2b 10 |
. . . . . . 7
   
              
           |
29 | | fvres 5893 |
. . . . . . . . . 10
        
            |
30 | 29 | eleq1d 2533 |
. . . . . . . . 9
                       |
31 | | 1st2nd2 6849 |
. . . . . . . . . 10
                  |
32 | | xp1st 6842 |
. . . . . . . . . 10
            |
33 | | elxp6 6844 |
. . . . . . . . . . . 12
   
                          |
34 | | anass 661 |
. . . . . . . . . . . 12
             
          
                          |
35 | 33, 34 | bitr4i 260 |
. . . . . . . . . . 11
   
            
             |
36 | 35 | baib 919 |
. . . . . . . . . 10
            
         
       |
37 | 31, 32, 36 | syl2anc 673 |
. . . . . . . . 9
                |
38 | 30, 37 | bitr4d 264 |
. . . . . . . 8
                      |
39 | 38 | pm5.32i 649 |
. . . . . . 7
                            |
40 | 28, 39 | bitri 257 |
. . . . . 6
   
                   |
41 | 25, 40 | syl6rbbr 272 |
. . . . 5
 
      
            |
42 | 41 | eqrdv 2469 |
. . . 4
 
     
           |
43 | 2 | adantr 472 |
. . . . 5
 
 
sigAlgebra |
44 | 3 | adantr 472 |
. . . . 5
 
 
sigAlgebra |
45 | | eqid 2471 |
. . . . . . . 8
   |
46 | | issgon 29019 |
. . . . . . . . 9
 sigAlgebra     sigAlgebra      |
47 | 46 | biimpri 211 |
. . . . . . . 8
   sigAlgebra   
sigAlgebra     |
48 | 2, 45, 47 | sylancl 675 |
. . . . . . 7
 sigAlgebra     |
49 | | baselsiga 29011 |
. . . . . . 7
 sigAlgebra      |
50 | 48, 49 | syl 17 |
. . . . . 6
    |
51 | 50 | adantr 472 |
. . . . 5
 
    |
52 | | simpr 468 |
. . . . 5
 
   |
53 | | elsx 29090 |
. . . . 5
    sigAlgebra
 sigAlgebra  
      ×s    |
54 | 43, 44, 51, 52, 53 | syl22anc 1293 |
. . . 4
 
  
  ×s    |
55 | 42, 54 | eqeltrd 2549 |
. . 3
 
     
       ×s    |
56 | 55 | ralrimiva 2809 |
. 2
      
       ×s    |
57 | 11, 3 | ismbfm 29147 |
. 2
    
    
×s  MblFnM    
      
×s        
       ×s      |
58 | 15, 56, 57 | mpbir2and 936 |
1
   
    
×s  MblFnM   |