Step | Hyp | Ref
| Expression |
1 | | bren 7575 |
. . 3

       |
2 | | elpwi 3959 |
. . . . . . 7
  
   |
3 | | imauni 6149 |
. . . . . . . . . . 11
              
          |
4 | | vex 3047 |
. . . . . . . . . . . . 13
 |
5 | | imaexg 6727 |
. . . . . . . . . . . . 13
       |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . . . . 12
     |
7 | 6 | dfiun2 4311 |
. . . . . . . . . . 11
  
                   
      |
8 | 3, 7 | eqtri 2472 |
. . . . . . . . . 10
                
            |
9 | | imaeq2 5163 |
. . . . . . . . . . . . . . 15
           |
10 | 9 | eleq1d 2512 |
. . . . . . . . . . . . . 14
     
       |
11 | 10 | rexrab 3201 |
. . . . . . . . . . . . 13
             
              |
12 | | eleq1 2516 |
. . . . . . . . . . . . . . . 16
     
       |
13 | 12 | biimparc 490 |
. . . . . . . . . . . . . . 15
     
       |
14 | 13 | rexlimivw 2875 |
. . . . . . . . . . . . . 14
       
    
  |
15 | | cnvimass 5187 |
. . . . . . . . . . . . . . . . . 18
    
 |
16 | | f1odm 5816 |
. . . . . . . . . . . . . . . . . . 19
    
  |
17 | 16 | ad3antrrr 735 |
. . . . . . . . . . . . . . . . . 18
        FinII  
 [ ]   
   |
18 | 15, 17 | syl5sseq 3479 |
. . . . . . . . . . . . . . . . 17
        FinII  
 [ ]   
        |
19 | 4 | cnvex 6737 |
. . . . . . . . . . . . . . . . . . 19
  |
20 | | imaexg 6727 |
. . . . . . . . . . . . . . . . . . 19
         |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
      |
22 | 21 | elpw 3956 |
. . . . . . . . . . . . . . . . 17
           
  |
23 | 18, 22 | sylibr 216 |
. . . . . . . . . . . . . . . 16
        FinII  
 [ ]   
         |
24 | | f1ofo 5819 |
. . . . . . . . . . . . . . . . . . . 20
    
      |
25 | 24 | ad3antrrr 735 |
. . . . . . . . . . . . . . . . . . 19
        FinII  
 [ ]   
       |
26 | | simprl 763 |
. . . . . . . . . . . . . . . . . . . . 21
      
FinII 
  [ ]       |
27 | 26 | sselda 3431 |
. . . . . . . . . . . . . . . . . . . 20
        FinII  
 [ ]   
    |
28 | 27 | elpwid 3960 |
. . . . . . . . . . . . . . . . . . 19
        FinII  
 [ ]   

  |
29 | | foimacnv 5829 |
. . . . . . . . . . . . . . . . . . 19
     
            |
30 | 25, 28, 29 | syl2anc 666 |
. . . . . . . . . . . . . . . . . 18
        FinII  
 [ ]   
            |
31 | 30 | eqcomd 2456 |
. . . . . . . . . . . . . . . . 17
        FinII  
 [ ]   
            |
32 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
        FinII  
 [ ]   
   |
33 | 31, 32 | eqeltrrd 2529 |
. . . . . . . . . . . . . . . 16
        FinII  
 [ ]   
            |
34 | | imaeq2 5163 |
. . . . . . . . . . . . . . . . . . 19
                     |
35 | 34 | eleq1d 2512 |
. . . . . . . . . . . . . . . . . 18
                       |
36 | 34 | eqeq2d 2460 |
. . . . . . . . . . . . . . . . . 18
                       |
37 | 35, 36 | anbi12d 716 |
. . . . . . . . . . . . . . . . 17
                
         
             |
38 | 37 | rspcev 3149 |
. . . . . . . . . . . . . . . 16
                            
              |
39 | 23, 33, 31, 38 | syl12anc 1265 |
. . . . . . . . . . . . . . 15
        FinII  
 [ ]   
               |
40 | 39 | ex 436 |
. . . . . . . . . . . . . 14
      
FinII 
  [ ]                    |
41 | 14, 40 | impbid2 208 |
. . . . . . . . . . . . 13
      
FinII 
  [ ]                
   |
42 | 11, 41 | syl5bb 261 |
. . . . . . . . . . . 12
      
FinII 
  [ ]       
         
   |
43 | 42 | abbi1dv 2570 |
. . . . . . . . . . 11
      
FinII 
  [ ]    

               |
44 | 43 | unieqd 4207 |
. . . . . . . . . 10
      
FinII 
  [ ]      
                |
45 | 8, 44 | syl5eq 2496 |
. . . . . . . . 9
      
FinII 
  [ ]         
         |
46 | | simplr 761 |
. . . . . . . . . . 11
      
FinII 
  [ ]   
FinII |
47 | | ssrab2 3513 |
. . . . . . . . . . . 12
         |
48 | 47 | a1i 11 |
. . . . . . . . . . 11
      
FinII 
  [ ]     
        |
49 | | simprrl 773 |
. . . . . . . . . . . . . 14
      
FinII 
  [ ]      |
50 | | n0 3740 |
. . . . . . . . . . . . . 14
    |
51 | 49, 50 | sylib 200 |
. . . . . . . . . . . . 13
      
FinII 
  [ ]    
  |
52 | | imaeq2 5163 |
. . . . . . . . . . . . . . . 16
                     |
53 | 52 | eleq1d 2512 |
. . . . . . . . . . . . . . 15
                       |
54 | 53 | rspcev 3149 |
. . . . . . . . . . . . . 14
                          |
55 | 23, 33, 54 | syl2anc 666 |
. . . . . . . . . . . . 13
        FinII  
 [ ]   
         |
56 | 51, 55 | exlimddv 1780 |
. . . . . . . . . . . 12
      
FinII 
  [ ]    
       |
57 | | rabn0 3751 |
. . . . . . . . . . . 12
                |
58 | 56, 57 | sylibr 216 |
. . . . . . . . . . 11
      
FinII 
  [ ]     
       |
59 | 10 | elrab 3195 |
. . . . . . . . . . . . . . 15
       
         |
60 | | imaeq2 5163 |
. . . . . . . . . . . . . . . . 17
           |
61 | 60 | eleq1d 2512 |
. . . . . . . . . . . . . . . 16
     
       |
62 | 61 | elrab 3195 |
. . . . . . . . . . . . . . 15
       
         |
63 | 59, 62 | anbi12i 702 |
. . . . . . . . . . . . . 14
        
                          |
64 | | simprrr 774 |
. . . . . . . . . . . . . . . . 17
      
FinII 
  [ ]    [ ]   |
65 | 64 | adantr 467 |
. . . . . . . . . . . . . . . 16
        FinII  
 [ ]            
        [ ]   |
66 | | simprlr 772 |
. . . . . . . . . . . . . . . 16
        FinII  
 [ ]            
              |
67 | | simprrr 774 |
. . . . . . . . . . . . . . . 16
        FinII  
 [ ]            
              |
68 | | sorpssi 6574 |
. . . . . . . . . . . . . . . 16
 [ ]           
                    |
69 | 65, 66, 67, 68 | syl12anc 1265 |
. . . . . . . . . . . . . . 15
        FinII  
 [ ]            
                            |
70 | | f1of1 5811 |
. . . . . . . . . . . . . . . . . 18
    
      |
71 | 70 | ad3antrrr 735 |
. . . . . . . . . . . . . . . . 17
        FinII  
 [ ]            
              |
72 | | simprll 771 |
. . . . . . . . . . . . . . . . . 18
        FinII  
 [ ]            
           |
73 | 72 | elpwid 3960 |
. . . . . . . . . . . . . . . . 17
        FinII  
 [ ]            
       
  |
74 | | simprrl 773 |
. . . . . . . . . . . . . . . . . 18
        FinII  
 [ ]            
       
   |
75 | 74 | elpwid 3960 |
. . . . . . . . . . . . . . . . 17
        FinII  
 [ ]            
          |
76 | | f1imass 6163 |
. . . . . . . . . . . . . . . . 17
      
 
        
   |
77 | 71, 73, 75, 76 | syl12anc 1265 |
. . . . . . . . . . . . . . . 16
        FinII  
 [ ]            
                
   |
78 | | f1imass 6163 |
. . . . . . . . . . . . . . . . 17
      
 
        
   |
79 | 71, 75, 73, 78 | syl12anc 1265 |
. . . . . . . . . . . . . . . 16
        FinII  
 [ ]            
                
   |
80 | 77, 79 | orbi12d 715 |
. . . . . . . . . . . . . . 15
        FinII  
 [ ]            
                          
     |
81 | 69, 80 | mpbid 214 |
. . . . . . . . . . . . . 14
        FinII  
 [ ]            
        
   |
82 | 63, 81 | sylan2b 478 |
. . . . . . . . . . . . 13
        FinII  
 [ ]                     
   |
83 | 82 | ralrimivva 2808 |
. . . . . . . . . . . 12
      
FinII 
  [ ]    
        
       
   |
84 | | sorpss 6573 |
. . . . . . . . . . . 12
[ ]  
    
  
        
         |
85 | 83, 84 | sylibr 216 |
. . . . . . . . . . 11
      
FinII 
  [ ]    [ ]          |
86 | | fin2i 8722 |
. . . . . . . . . . 11
   FinII                 
[ ]            
              |
87 | 46, 48, 58, 85, 86 | syl22anc 1268 |
. . . . . . . . . 10
      
FinII 
  [ ]      
              |
88 | | imaeq2 5163 |
. . . . . . . . . . . . 13
                           |
89 | 88 | eleq1d 2512 |
. . . . . . . . . . . 12
                             |
90 | 10 | cbvrabv 3043 |
. . . . . . . . . . . 12
        
      |
91 | 89, 90 | elrab2 3197 |
. . . . . . . . . . 11
   
                                     |
92 | 91 | simprbi 466 |
. . . . . . . . . 10
   
                 
        |
93 | 87, 92 | syl 17 |
. . . . . . . . 9
      
FinII 
  [ ]         
        |
94 | 45, 93 | eqeltrrd 2529 |
. . . . . . . 8
      
FinII 
  [ ]    
  |
95 | 94 | expr 619 |
. . . . . . 7
      
FinII    
[ ] 
    |
96 | 2, 95 | sylan2 477 |
. . . . . 6
      
FinII
     [ ] 
    |
97 | 96 | ralrimiva 2801 |
. . . . 5
     
FinII      [ ] 
    |
98 | 97 | ex 436 |
. . . 4
    
 FinII     
[ ] 
     |
99 | 98 | exlimiv 1775 |
. . 3
       FinII      [ ] 
     |
100 | 1, 99 | sylbi 199 |
. 2
 
FinII     
[ ] 
     |
101 | | relen 7571 |
. . . 4
 |
102 | 101 | brrelex2i 4875 |
. . 3
   |
103 | | isfin2 8721 |
. . 3
 
FinII     
[ ] 
     |
104 | 102, 103 | syl 17 |
. 2
 
FinII     
[ ] 
     |
105 | 100, 104 | sylibrd 238 |
1
 
FinII FinII  |