Step | Hyp | Ref
| Expression |
1 | | sltirr 30559 |
. . . . . . . . 9
      |
2 | | breq2 4406 |
. . . . . . . . . 10
    
      |
3 | 2 | notbid 296 |
. . . . . . . . 9
           |
4 | 1, 3 | syl5ibcom 224 |
. . . . . . . 8
 
      |
5 | 4 | con2d 119 |
. . . . . . 7
    
   |
6 | 5 | imp 431 |
. . . . . 6
     
  |
7 | 6 | ad2ant2rl 755 |
. . . . 5
         
  |
8 | | nofun 30536 |
. . . . . . . . 9
   |
9 | | nofun 30536 |
. . . . . . . . 9
   |
10 | | eqfunfv 5981 |
. . . . . . . . 9
  

 
             |
11 | 8, 9, 10 | syl2an 480 |
. . . . . . . 8
 
  
              |
12 | 11 | notbid 296 |
. . . . . . 7
 
 
               |
13 | 12 | adantr 467 |
. . . . . 6
          
               |
14 | | imnan 424 |
. . . . . . . . . . . 12
 
          
              |
15 | 14 | biimpri 210 |
. . . . . . . . . . 11
  
          
             |
16 | 15 | impcom 432 |
. . . . . . . . . 10
              
            |
17 | | df-ne 2624 |
. . . . . . . . . . . . 13
        
          |
18 | 17 | rexbii 2889 |
. . . . . . . . . . . 12
          
           |
19 | | rexnal 2836 |
. . . . . . . . . . . 12
         
            |
20 | 18, 19 | bitri 253 |
. . . . . . . . . . 11
          
            |
21 | | nodenselem4 30573 |
. . . . . . . . . . . . . . 15
                     |
22 | | eloni 5433 |
. . . . . . . . . . . . . . 15
                         |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . 14
                     |
24 | 23 | adantr 467 |
. . . . . . . . . . . . 13
         
                       |
25 | | nodmord 30540 |
. . . . . . . . . . . . . 14
   |
26 | 25 | ad3antrrr 736 |
. . . . . . . . . . . . 13
         
            |
27 | | nodmon 30537 |
. . . . . . . . . . . . . . . . . . 19
   |
28 | | onelon 5448 |
. . . . . . . . . . . . . . . . . . 19
  
  |
29 | 27, 28 | sylan 474 |
. . . . . . . . . . . . . . . . . 18
 
   |
30 | 29 | ex 436 |
. . . . . . . . . . . . . . . . 17
     |
31 | 30 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
            |
32 | 31 | anim1d 568 |
. . . . . . . . . . . . . . 15
                  
             |
33 | 32 | imp 431 |
. . . . . . . . . . . . . 14
         
                      |
34 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
           |
35 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
           |
36 | 34, 35 | neeq12d 2685 |
. . . . . . . . . . . . . . 15
         
           |
37 | 36 | intminss 4261 |
. . . . . . . . . . . . . 14
                        |
38 | 33, 37 | syl 17 |
. . . . . . . . . . . . 13
         
                       |
39 | | simprl 764 |
. . . . . . . . . . . . 13
         
            |
40 | | ordtr2 5467 |
. . . . . . . . . . . . . 14
                          

              |
41 | 40 | imp 431 |
. . . . . . . . . . . . 13
                          
               |
42 | 24, 26, 38, 39, 41 | syl22anc 1269 |
. . . . . . . . . . . 12
         
                       |
43 | 42 | rexlimdvaa 2880 |
. . . . . . . . . . 11
         
                   
   |
44 | 20, 43 | syl5bir 222 |
. . . . . . . . . 10
                             
   |
45 | 16, 44 | syl5 33 |
. . . . . . . . 9
         
            
              |
46 | 45 | exp4b 612 |
. . . . . . . 8
 
    
                              |
47 | 46 | com23 81 |
. . . . . . 7
 
                                   |
48 | 47 | imp32 435 |
. . . . . 6
                                     |
49 | 13, 48 | sylbid 219 |
. . . . 5
          
              |
50 | 7, 49 | mpd 15 |
. . . 4
                       |
51 | 50 | ex 436 |
. . 3
 
                 
   |
52 | | bdayval 30535 |
. . . . 5
       |
53 | | bdayval 30535 |
. . . . 5
       |
54 | 52, 53 | eqeqan12d 2467 |
. . . 4
 
         
   |
55 | 54 | anbi1d 711 |
. . 3
 
                       |
56 | 52 | eleq2d 2514 |
. . . 4
            
   
              |
57 | 56 | adantr 467 |
. . 3
 
                           
   |
58 | 51, 55, 57 | 3imtr4d 272 |
. 2
 
              
                  |
59 | 58 | imp 431 |
1
                                   |