Step | Hyp | Ref
| Expression |
1 | | ennnfone 12426 |
. . . 4

 

DECID
                           |
2 | 1 | simplbi 274 |
. . 3



DECID
  |
3 | | nnenom 10434 |
. . . . . . 7
 |
4 | | entr 6784 |
. . . . . . 7
     |
5 | 3, 4 | mpan2 425 |
. . . . . 6

  |
6 | 5 | ensymd 6783 |
. . . . 5

  |
7 | | bren 6747 |
. . . . 5

       |
8 | 6, 7 | sylib 122 |
. . . 4

       |
9 | | f1ofo 5469 |
. . . . . . . 8
    
      |
10 | 9 | adantl 277 |
. . . . . . 7
             |
11 | | simpr 110 |
. . . . . . . . 9
           |
12 | | nnord 4612 |
. . . . . . . . . . . 12
   |
13 | 12 | adantl 277 |
. . . . . . . . . . 11
           |
14 | | ordirr 4542 |
. . . . . . . . . . 11

  |
15 | 13, 14 | syl 14 |
. . . . . . . . . 10
        
  |
16 | | f1of1 5461 |
. . . . . . . . . . . 12
    
      |
17 | 16 | ad2antlr 489 |
. . . . . . . . . . 11
               |
18 | | omelon 4609 |
. . . . . . . . . . . . 13
 |
19 | 18 | onelssi 4430 |
. . . . . . . . . . . 12
   |
20 | 19 | adantl 277 |
. . . . . . . . . . 11
           |
21 | | f1elima 5774 |
. . . . . . . . . . 11
     
             |
22 | 17, 11, 20, 21 | syl3anc 1238 |
. . . . . . . . . 10
                 
   |
23 | 15, 22 | mtbird 673 |
. . . . . . . . 9
                   |
24 | | fveq2 5516 |
. . . . . . . . . . . 12
           |
25 | 24 | eleq1d 2246 |
. . . . . . . . . . 11
         
           |
26 | 25 | notbid 667 |
. . . . . . . . . 10
         
           |
27 | 26 | rspcev 2842 |
. . . . . . . . 9
                      |
28 | 11, 23, 27 | syl2anc 411 |
. . . . . . . 8
                    |
29 | 28 | ralrimiva 2550 |
. . . . . . 7
        
          |
30 | 10, 29 | jca 306 |
. . . . . 6
                         |
31 | 30 | ex 115 |
. . . . 5

    
    
 
            |
32 | 31 | eximdv 1880 |
. . . 4

              
            |
33 | 8, 32 | mpd 13 |
. . 3

                    |
34 | 2, 33 | jca 306 |
. 2

 

DECID
                     |
35 | | oveq1 5882 |
. . . . . . . . 9
       |
36 | 35 | cbvmptv 4100 |
. . . . . . . 8
         |
37 | | freceq1 6393 |
. . . . . . . 8
         frec       frec         |
38 | 36, 37 | ax-mp 5 |
. . . . . . 7
frec       frec        |
39 | | eqid 2177 |
. . . . . . 7
 frec         frec         |
40 | | simpl 109 |
. . . . . . 7
                       |
41 | | fveq2 5516 |
. . . . . . . . . . . . 13
           |
42 | 41 | eleq1d 2246 |
. . . . . . . . . . . 12
         
           |
43 | 42 | notbid 667 |
. . . . . . . . . . 11
         
           |
44 | 43 | cbvrexv 2705 |
. . . . . . . . . 10
         
           |
45 | 44 | ralbii 2483 |
. . . . . . . . 9
 
                     |
46 | | imaeq2 4967 |
. . . . . . . . . . . . 13
           |
47 | 46 | eleq2d 2247 |
. . . . . . . . . . . 12
         
           |
48 | 47 | notbid 667 |
. . . . . . . . . . 11
         
           |
49 | 48 | rexbidv 2478 |
. . . . . . . . . 10
  
       
            |
50 | 49 | cbvralv 2704 |
. . . . . . . . 9
 
                     |
51 | 45, 50 | sylbb 123 |
. . . . . . . 8
 
        
 
          |
52 | 51 | adantl 277 |
. . . . . . 7
                             |
53 | 38, 39, 40, 52 | ctinfomlemom 12428 |
. . . . . 6
                   frec                      frec             frec              |
54 | | vex 2741 |
. . . . . . . 8
 |
55 | | frecex 6395 |
. . . . . . . . 9
frec        |
56 | 55 | cnvex 5168 |
. . . . . . . 8
frec        |
57 | 54, 56 | coex 5175 |
. . . . . . 7
 frec         |
58 | | foeq1 5435 |
. . . . . . . 8
  frec              frec               |
59 | | fveq1 5515 |
. . . . . . . . . . . 12
  frec              frec             |
60 | | fveq1 5515 |
. . . . . . . . . . . 12
  frec              frec             |
61 | 59, 60 | neeq12d 2367 |
. . . . . . . . . . 11
  frec                   frec             frec              |
62 | 61 | ralbidv 2477 |
. . . . . . . . . 10
  frec                               frec             frec              |
63 | 62 | rexbidv 2478 |
. . . . . . . . 9
  frec                       
         frec             frec              |
64 | 63 | ralbidv 2477 |
. . . . . . . 8
  frec                        
          frec             frec              |
65 | 58, 64 | anbi12d 473 |
. . . . . . 7
  frec             
                   frec           
          frec             frec               |
66 | 57, 65 | spcev 2833 |
. . . . . 6
   frec           
          frec             frec                  
                   |
67 | 53, 66 | syl 14 |
. . . . 5
                                           |
68 | 67 | exlimiv 1598 |
. . . 4
       
 
        
                          |
69 | 68 | anim2i 342 |
. . 3
   
DECID
                  
 

DECID
                           |
70 | 69, 1 | sylibr 134 |
. 2
   
DECID
                  
  |
71 | 34, 70 | impbii 126 |
1

 

DECID
        
            |