Step | Hyp | Ref
| Expression |
1 | | f1stres 6834 |
. . . 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 | 2, 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 | 2, 16, 17, 19 | 4syl 19 |
. . . . . . . . . 10
     |
21 | 20 | r19.21bi 2776 |
. . . . . . . . 9
 
    |
22 | | xpss1 4948 |
. . . . . . . . 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 | | xp2nd 6843 |
. . . . . . . . . 10
            |
33 | | elxp6 6844 |
. . . . . . . . . . . 12
   
                          |
34 | | anass 661 |
. . . . . . . . . . . 12
             
          
                          |
35 | | an32 815 |
. . . . . . . . . . . 12
             
          
            
             |
36 | 33, 34, 35 | 3bitr2i 281 |
. . . . . . . . . . 11
   
            
             |
37 | 36 | baib 919 |
. . . . . . . . . 10
            
                 |
38 | 31, 32, 37 | syl2anc 673 |
. . . . . . . . 9
                |
39 | 30, 38 | bitr4d 264 |
. . . . . . . 8
                      |
40 | 39 | pm5.32i 649 |
. . . . . . 7
                            |
41 | 28, 40 | bitri 257 |
. . . . . 6
   
                   |
42 | 25, 41 | syl6rbbr 272 |
. . . . 5
 
      
            |
43 | 42 | eqrdv 2469 |
. . . 4
 
     
           |
44 | 2 | adantr 472 |
. . . . 5
 
 
sigAlgebra |
45 | 3 | adantr 472 |
. . . . 5
 
 
sigAlgebra |
46 | | simpr 468 |
. . . . 5
 
   |
47 | | eqid 2471 |
. . . . . . . 8
   |
48 | | issgon 29019 |
. . . . . . . . 9
 sigAlgebra     sigAlgebra      |
49 | 48 | biimpri 211 |
. . . . . . . 8
   sigAlgebra   
sigAlgebra     |
50 | 3, 47, 49 | sylancl 675 |
. . . . . . 7
 sigAlgebra     |
51 | | baselsiga 29011 |
. . . . . . 7
 sigAlgebra      |
52 | 50, 51 | syl 17 |
. . . . . 6
    |
53 | 52 | adantr 472 |
. . . . 5
 
    |
54 | | elsx 29090 |
. . . . 5
    sigAlgebra
 sigAlgebra         ×s    |
55 | 44, 45, 46, 53, 54 | syl22anc 1293 |
. . . 4
 
     ×s    |
56 | 43, 55 | eqeltrd 2549 |
. . 3
 
     
       ×s    |
57 | 56 | ralrimiva 2809 |
. 2
      
       ×s    |
58 | 11, 2 | ismbfm 29147 |
. 2
    
    
×s  MblFnM    
      
×s        
       ×s      |
59 | 15, 57, 58 | mpbir2and 936 |
1
   
    
×s  MblFnM   |