Step | Hyp | Ref
| Expression |
1 | | isfi 7618 |
. . 3

   |
2 | | bren 7603 |
. . . . 5

       |
3 | | f1ofo 5843 |
. . . . . . . . . . 11
    
      |
4 | | imassrn 5197 |
. . . . . . . . . . . 12
     |
5 | | forn 5818 |
. . . . . . . . . . . 12
    
  |
6 | 4, 5 | syl5sseq 3491 |
. . . . . . . . . . 11
        
  |
7 | 3, 6 | syl 17 |
. . . . . . . . . 10
    
      |
8 | | ssnnfi 7816 |
. . . . . . . . . . 11
     
       |
9 | | isfi 7618 |
. . . . . . . . . . 11
    
       |
10 | 8, 9 | sylib 201 |
. . . . . . . . . 10
     
     
  |
11 | 7, 10 | sylan2 481 |
. . . . . . . . 9
              |
12 | 11 | adantrr 728 |
. . . . . . . 8
      
 
       |
13 | | f1of1 5835 |
. . . . . . . . . . . . . 14
    
      |
14 | | f1ores 5850 |
. . . . . . . . . . . . . 14
     
             |
15 | 13, 14 | sylan 478 |
. . . . . . . . . . . . 13
                   |
16 | | vex 3059 |
. . . . . . . . . . . . . . . . 17
 |
17 | 16 | resex 5166 |
. . . . . . . . . . . . . . . 16
   |
18 | | f1oeq1 5827 |
. . . . . . . . . . . . . . . 16
           
             |
19 | 17, 18 | spcev 3152 |
. . . . . . . . . . . . . . 15
 
        
           |
20 | | bren 7603 |
. . . . . . . . . . . . . . 15
    
           |
21 | 19, 20 | sylibr 217 |
. . . . . . . . . . . . . 14
 
        
      |
22 | | entr 7646 |
. . . . . . . . . . . . . 14
         
   |
23 | 21, 22 | sylan 478 |
. . . . . . . . . . . . 13
           
    
  |
24 | 15, 23 | sylan 478 |
. . . . . . . . . . . 12
      
     
  |
25 | 24 | ex 440 |
. . . . . . . . . . 11
               |
26 | 25 | reximdv 2872 |
. . . . . . . . . 10
                 |
27 | | isfi 7618 |
. . . . . . . . . 10

   |
28 | 26, 27 | syl6ibr 235 |
. . . . . . . . 9
                |
29 | 28 | adantl 472 |
. . . . . . . 8
      
 
 
       |
30 | 12, 29 | mpd 15 |
. . . . . . 7
      
 
  |
31 | 30 | exp32 614 |
. . . . . 6
           |
32 | 31 | exlimdv 1789 |
. . . . 5
  
         |
33 | 2, 32 | syl5bi 225 |
. . . 4
       |
34 | 33 | rexlimiv 2884 |
. . 3
 
    |
35 | 1, 34 | sylbi 200 |
. 2
     |
36 | 35 | imp 435 |
1
  
  |