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

   |
2 | | relen 7592 |
. . . . . . . . 9
 |
3 | 2 | brrelexi 4880 |
. . . . . . . 8
   |
4 | | pssss 3514 |
. . . . . . . 8
   |
5 | | ssdomg 7633 |
. . . . . . . . 9
     |
6 | 5 | imp 436 |
. . . . . . . 8
     |
7 | 3, 4, 6 | syl2an 485 |
. . . . . . 7
     |
8 | 7 | adantll 728 |
. . . . . 6
    
  |
9 | | bren 7596 |
. . . . . . . . 9

       |
10 | | imass2 5210 |
. . . . . . . . . . . . . . . . 17
           |
11 | 4, 10 | syl 17 |
. . . . . . . . . . . . . . . 16
           |
12 | 11 | adantl 473 |
. . . . . . . . . . . . . . 15
          
      |
13 | | pssnel 3829 |
. . . . . . . . . . . . . . . . 17
       |
14 | | eldif 3400 |
. . . . . . . . . . . . . . . . . . . 20
  

   |
15 | | f1ofn 5829 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
  |
16 | | difss 3549 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
17 | | fnfvima 6161 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
                |
18 | 17 | 3expia 1233 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
                  |
19 | 15, 16, 18 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . 22
    
                |
20 | | dff1o3 5834 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
    
    |
21 | 20 | simprbi 471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
   |
22 | | imadif 5668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
                  |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
                  |
24 | 23 | eleq2d 2534 |
. . . . . . . . . . . . . . . . . . . . . 22
    
          
        
        |
25 | 19, 24 | sylibd 222 |
. . . . . . . . . . . . . . . . . . . . 21
    
                    |
26 | | n0i 3727 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
27 | 25, 26 | syl6 33 |
. . . . . . . . . . . . . . . . . . . 20
    
                |
28 | 14, 27 | syl5bir 226 |
. . . . . . . . . . . . . . . . . . 19
    
 

    
        |
29 | 28 | exlimdv 1787 |
. . . . . . . . . . . . . . . . . 18
    
                  |
30 | 29 | imp 436 |
. . . . . . . . . . . . . . . . 17
                       |
31 | 13, 30 | sylan2 482 |
. . . . . . . . . . . . . . . 16
                   |
32 | | ssdif0 3741 |
. . . . . . . . . . . . . . . 16
        
            |
33 | 31, 32 | sylnibr 312 |
. . . . . . . . . . . . . . 15
          
      |
34 | | dfpss3 3505 |
. . . . . . . . . . . . . . 15
        
            
       |
35 | 12, 33, 34 | sylanbrc 677 |
. . . . . . . . . . . . . 14
          
      |
36 | | imadmrn 5184 |
. . . . . . . . . . . . . . . . 17
  
  |
37 | | f1odm 5832 |
. . . . . . . . . . . . . . . . . 18
    
  |
38 | 37 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . 17
    
  
       |
39 | | f1ofo 5835 |
. . . . . . . . . . . . . . . . . 18
    
      |
40 | | forn 5809 |
. . . . . . . . . . . . . . . . . 18
    
  |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . . 17
    
  |
42 | 36, 38, 41 | 3eqtr3a 2529 |
. . . . . . . . . . . . . . . 16
    
      |
43 | 42 | psseq2d 3512 |
. . . . . . . . . . . . . . 15
    
        
       |
44 | 43 | adantr 472 |
. . . . . . . . . . . . . 14
                   
   |
45 | 35, 44 | mpbid 215 |
. . . . . . . . . . . . 13
          
  |
46 | | php 7774 |
. . . . . . . . . . . . 13
     
       |
47 | 45, 46 | sylan2 482 |
. . . . . . . . . . . 12
      
 
      |
48 | | f1of1 5827 |
. . . . . . . . . . . . . . . 16
    
      |
49 | | f1ores 5842 |
. . . . . . . . . . . . . . . 16
     
             |
50 | 48, 4, 49 | syl2an 485 |
. . . . . . . . . . . . . . 15
                   |
51 | | vex 3034 |
. . . . . . . . . . . . . . . . . 18
 |
52 | 51 | resex 5154 |
. . . . . . . . . . . . . . . . 17
   |
53 | | f1oeq1 5818 |
. . . . . . . . . . . . . . . . 17
           
             |
54 | 52, 53 | spcev 3127 |
. . . . . . . . . . . . . . . 16
 
        
           |
55 | | bren 7596 |
. . . . . . . . . . . . . . . 16
    
           |
56 | 54, 55 | sylibr 217 |
. . . . . . . . . . . . . . 15
 
        
      |
57 | 50, 56 | syl 17 |
. . . . . . . . . . . . . 14
             |
58 | | entr 7639 |
. . . . . . . . . . . . . . 15
             |
59 | 58 | expcom 442 |
. . . . . . . . . . . . . 14
     
       |
60 | 57, 59 | syl 17 |
. . . . . . . . . . . . 13
               |
61 | 60 | adantl 473 |
. . . . . . . . . . . 12
      
 

       |
62 | 47, 61 | mtod 182 |
. . . . . . . . . . 11
      
 
  |
63 | 62 | exp32 616 |
. . . . . . . . . 10
           |
64 | 63 | exlimdv 1787 |
. . . . . . . . 9
  
    
    |
65 | 9, 64 | syl5bi 225 |
. . . . . . . 8
       |
66 | 65 | imp31 439 |
. . . . . . 7
    
  |
67 | | entr 7639 |
. . . . . . . . . 10
     |
68 | 67 | ex 441 |
. . . . . . . . 9
     |
69 | | ensym 7636 |
. . . . . . . . 9
   |
70 | 68, 69 | syl6com 35 |
. . . . . . . 8
     |
71 | 70 | ad2antlr 741 |
. . . . . . 7
    

   |
72 | 66, 71 | mtod 182 |
. . . . . 6
    
  |
73 | | brsdom 7610 |
. . . . . 6

    |
74 | 8, 72, 73 | sylanbrc 677 |
. . . . 5
    
  |
75 | 74 | exp31 615 |
. . . 4
       |
76 | 75 | rexlimiv 2867 |
. . 3
 
    |
77 | 1, 76 | sylbi 200 |
. 2
     |
78 | 77 | imp 436 |
1
     |