Step | Hyp | Ref
| Expression |
1 | | ensym 7615 |
. 2
   |
2 | | bren 7575 |
. . . 4

       |
3 | | simpr 463 |
. . . . . . . . . . . 12
         |
4 | | f1of1 5811 |
. . . . . . . . . . . . 13
    
      |
5 | | pssss 3527 |
. . . . . . . . . . . . . 14
   |
6 | | ssid 3450 |
. . . . . . . . . . . . . 14
 |
7 | 5, 6 | jctir 541 |
. . . . . . . . . . . . 13
 
   |
8 | | f1imapss 6165 |
. . . . . . . . . . . . 13
      
 
        
   |
9 | 4, 7, 8 | syl2an 480 |
. . . . . . . . . . . 12
               
   |
10 | 3, 9 | mpbird 236 |
. . . . . . . . . . 11
          
      |
11 | | imadmrn 5177 |
. . . . . . . . . . . . . 14
  
  |
12 | | f1odm 5816 |
. . . . . . . . . . . . . . 15
    
  |
13 | 12 | imaeq2d 5167 |
. . . . . . . . . . . . . 14
    
          |
14 | | dff1o5 5821 |
. . . . . . . . . . . . . . 15
         
   |
15 | 14 | simprbi 466 |
. . . . . . . . . . . . . 14
    
  |
16 | 11, 13, 15 | 3eqtr3a 2508 |
. . . . . . . . . . . . 13
    
      |
17 | 16 | adantr 467 |
. . . . . . . . . . . 12
             |
18 | 17 | psseq2d 3525 |
. . . . . . . . . . 11
                   
   |
19 | 10, 18 | mpbid 214 |
. . . . . . . . . 10
          
  |
20 | 19 | adantrr 722 |
. . . . . . . . 9
      
        |
21 | | vex 3047 |
. . . . . . . . . . . . . 14
 |
22 | 21 | f1imaen 7628 |
. . . . . . . . . . . . 13
     
       |
23 | 4, 5, 22 | syl2an 480 |
. . . . . . . . . . . 12
          
  |
24 | 23 | adantrr 722 |
. . . . . . . . . . 11
      
        |
25 | | simprr 765 |
. . . . . . . . . . 11
      
    |
26 | | entr 7618 |
. . . . . . . . . . 11
     
    
  |
27 | 24, 25, 26 | syl2anc 666 |
. . . . . . . . . 10
      
        |
28 | | vex 3047 |
. . . . . . . . . . . 12
 |
29 | | f1oen3g 7582 |
. . . . . . . . . . . 12
         |
30 | 28, 29 | mpan 675 |
. . . . . . . . . . 11
    
  |
31 | 30 | adantr 467 |
. . . . . . . . . 10
      
    |
32 | | entr 7618 |
. . . . . . . . . 10
     
    
  |
33 | 27, 31, 32 | syl2anc 666 |
. . . . . . . . 9
      
        |
34 | | fin4i 8725 |
. . . . . . . . 9
     
   
 FinIV |
35 | 20, 33, 34 | syl2anc 666 |
. . . . . . . 8
      
 
FinIV |
36 | 35 | ex 436 |
. . . . . . 7
    
 

FinIV  |
37 | 36 | exlimdv 1778 |
. . . . . 6
    
    
FinIV  |
38 | 37 | con2d 119 |
. . . . 5
    
 FinIV   
    |
39 | 38 | exlimiv 1775 |
. . . 4
       FinIV        |
40 | 2, 39 | sylbi 199 |
. . 3
 
FinIV
  
    |
41 | | relen 7571 |
. . . . 5
 |
42 | 41 | brrelexi 4874 |
. . . 4
   |
43 | | isfin4 8724 |
. . . 4
 
FinIV   
    |
44 | 42, 43 | syl 17 |
. . 3
 
FinIV   
    |
45 | 40, 44 | sylibrd 238 |
. 2
 
FinIV FinIV  |
46 | 1, 45 | syl 17 |
1
 
FinIV FinIV  |