Step | Hyp | Ref
| Expression |
1 | | ensym 7618 |
. . 3
   |
2 | | bren 7578 |
. . 3

       |
3 | 1, 2 | sylib 200 |
. 2
        |
4 | | elpwi 3960 |
. . . . . . 7
    |
5 | | simplr 762 |
. . . . . . . . 9
      
FinIa 
FinIa |
6 | | imassrn 5179 |
. . . . . . . . . 10
     |
7 | | f1of 5814 |
. . . . . . . . . . . 12
    
      |
8 | 7 | ad2antrr 732 |
. . . . . . . . . . 11
      
FinIa        |
9 | | frn 5735 |
. . . . . . . . . . 11
    
  |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
      
FinIa 
  |
11 | 6, 10 | syl5ss 3443 |
. . . . . . . . 9
      
FinIa     
  |
12 | | fin1ai 8723 |
. . . . . . . . 9
 
FinIa
          
        |
13 | 5, 11, 12 | syl2anc 667 |
. . . . . . . 8
      
FinIa                |
14 | | f1of1 5813 |
. . . . . . . . . . . 12
    
      |
15 | 14 | ad2antrr 732 |
. . . . . . . . . . 11
      
FinIa        |
16 | | simpr 463 |
. . . . . . . . . . 11
      
FinIa    |
17 | | vex 3048 |
. . . . . . . . . . . 12
 |
18 | 17 | a1i 11 |
. . . . . . . . . . 11
      
FinIa 
  |
19 | | f1imaeng 7629 |
. . . . . . . . . . 11
     
    
  |
20 | 15, 16, 18, 19 | syl3anc 1268 |
. . . . . . . . . 10
      
FinIa     
  |
21 | | enfi 7788 |
. . . . . . . . . 10
         
   |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
      
FinIa          |
23 | | df-f1 5587 |
. . . . . . . . . . . . . 14
    
         |
24 | 23 | simprbi 466 |
. . . . . . . . . . . . 13
        |
25 | | imadif 5658 |
. . . . . . . . . . . . 13
 
                  |
26 | 15, 24, 25 | 3syl 18 |
. . . . . . . . . . . 12
      
FinIa                    |
27 | | f1ofo 5821 |
. . . . . . . . . . . . . . 15
    
      |
28 | | foima 5798 |
. . . . . . . . . . . . . . 15
           |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . 14
    
      |
30 | 29 | ad2antrr 732 |
. . . . . . . . . . . . 13
      
FinIa        |
31 | 30 | difeq1d 3550 |
. . . . . . . . . . . 12
      
FinIa                    |
32 | 26, 31 | eqtrd 2485 |
. . . . . . . . . . 11
      
FinIa                |
33 | | difssd 3561 |
. . . . . . . . . . . 12
      
FinIa   
  |
34 | | vex 3048 |
. . . . . . . . . . . . . . 15
 |
35 | 7 | adantr 467 |
. . . . . . . . . . . . . . 15
     
FinIa       |
36 | | dmfex 6751 |
. . . . . . . . . . . . . . 15
         |
37 | 34, 35, 36 | sylancr 669 |
. . . . . . . . . . . . . 14
     
FinIa   |
38 | 37 | adantr 467 |
. . . . . . . . . . . . 13
      
FinIa 
  |
39 | | difexg 4551 |
. . . . . . . . . . . . 13
     |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . 12
      
FinIa      |
41 | | f1imaeng 7629 |
. . . . . . . . . . . 12
       

            |
42 | 15, 33, 40, 41 | syl3anc 1268 |
. . . . . . . . . . 11
      
FinIa            |
43 | 32, 42 | eqbrtrrd 4425 |
. . . . . . . . . 10
      
FinIa            |
44 | | enfi 7788 |
. . . . . . . . . 10
               
     |
45 | 43, 44 | syl 17 |
. . . . . . . . 9
      
FinIa              |
46 | 22, 45 | orbi12d 716 |
. . . . . . . 8
      
FinIa       
              |
47 | 13, 46 | mpbid 214 |
. . . . . . 7
      
FinIa        |
48 | 4, 47 | sylan2 477 |
. . . . . 6
      
FinIa
 
      |
49 | 48 | ralrimiva 2802 |
. . . . 5
     
FinIa         |
50 | | isfin1a 8722 |
. . . . . 6
 
FinIa   
      |
51 | 37, 50 | syl 17 |
. . . . 5
     
FinIa 
FinIa   
      |
52 | 49, 51 | mpbird 236 |
. . . 4
     
FinIa FinIa |
53 | 52 | ex 436 |
. . 3
    
 FinIa
FinIa  |
54 | 53 | exlimiv 1776 |
. 2
       FinIa FinIa  |
55 | 3, 54 | syl 17 |
1
 
FinIa FinIa  |