Step | Hyp | Ref
| Expression |
1 | | fidcenumlemr.f |
. . 3
       |
2 | | foima 5444 |
. . 3
           |
3 | 1, 2 | syl 14 |
. 2
       |
4 | | ssid 3176 |
. . 3
 |
5 | | fidcenumlemr.n |
. . . . 5
   |
6 | 5 | adantr 276 |
. . . 4
 

  |
7 | | sseq1 3179 |
. . . . . . 7


   |
8 | 7 | anbi2d 464 |
. . . . . 6

 
      |
9 | | imaeq2 4967 |
. . . . . . 7

          |
10 | 9 | eleq1d 2246 |
. . . . . 6

    
       |
11 | 8, 10 | imbi12d 234 |
. . . . 5

        
 
         |
12 | | sseq1 3179 |
. . . . . . 7
 
   |
13 | 12 | anbi2d 464 |
. . . . . 6
  


    |
14 | | imaeq2 4967 |
. . . . . . 7
           |
15 | 14 | eleq1d 2246 |
. . . . . 6
     
       |
16 | 13, 15 | imbi12d 234 |
. . . . 5
                     |
17 | | sseq1 3179 |
. . . . . . 7
 
   |
18 | 17 | anbi2d 464 |
. . . . . 6
   
     |
19 | | imaeq2 4967 |
. . . . . . 7
       
   |
20 | 19 | eleq1d 2246 |
. . . . . 6
             |
21 | 18, 20 | imbi12d 234 |
. . . . 5
   
                 |
22 | | sseq1 3179 |
. . . . . . 7
 
   |
23 | 22 | anbi2d 464 |
. . . . . 6
  


    |
24 | | imaeq2 4967 |
. . . . . . 7
           |
25 | 24 | eleq1d 2246 |
. . . . . 6
     
       |
26 | 23, 25 | imbi12d 234 |
. . . . 5
                     |
27 | | ima0 4988 |
. . . . . . 7
     |
28 | | 0fin 6884 |
. . . . . . 7
 |
29 | 27, 28 | eqeltri 2250 |
. . . . . 6
     |
30 | 29 | a1i 9 |
. . . . 5
 

      |
31 | | simprl 529 |
. . . . . . . . . . . . . 14
           
     |
32 | | fofn 5441 |
. . . . . . . . . . . . . . 15
    
  |
33 | 1, 32 | syl 14 |
. . . . . . . . . . . . . 14
   |
34 | 31, 33 | syl 14 |
. . . . . . . . . . . . 13
           
     |
35 | | simprr 531 |
. . . . . . . . . . . . . 14
           
     |
36 | | vex 2741 |
. . . . . . . . . . . . . . . 16
 |
37 | 36 | sucid 4418 |
. . . . . . . . . . . . . . 15
 |
38 | 37 | a1i 9 |
. . . . . . . . . . . . . 14
           
     |
39 | 35, 38 | sseldd 3157 |
. . . . . . . . . . . . 13
           
     |
40 | | fnsnfv 5576 |
. . . . . . . . . . . . 13
 
               |
41 | 34, 39, 40 | syl2anc 411 |
. . . . . . . . . . . 12
           
                 |
42 | 41 | uneq2d 3290 |
. . . . . . . . . . 11
           
                             |
43 | | df-suc 4372 |
. . . . . . . . . . . . 13
     |
44 | 43 | imaeq2i 4969 |
. . . . . . . . . . . 12
  
          |
45 | | imaundi 5042 |
. . . . . . . . . . . 12
                     |
46 | 44, 45 | eqtri 2198 |
. . . . . . . . . . 11
  
              |
47 | 42, 46 | eqtr4di 2228 |
. . . . . . . . . 10
           
                     |
48 | 47 | adantr 276 |
. . . . . . . . 9
   
  
                                    |
49 | | simpr 110 |
. . . . . . . . . . 11
   
  
                            |
50 | 49 | snssd 3738 |
. . . . . . . . . 10
   
  
                              |
51 | | ssequn2 3309 |
. . . . . . . . . 10
          
                  |
52 | 50, 51 | sylib 122 |
. . . . . . . . 9
   
  
                                    |
53 | 48, 52 | eqtr3d 2212 |
. . . . . . . 8
   
  
                            |
54 | | sssucid 4416 |
. . . . . . . . . . . 12
 |
55 | | sstr 3164 |
. . . . . . . . . . . 12
 
   |
56 | 54, 55 | mpan 424 |
. . . . . . . . . . 11

  |
57 | 56 | ad2antll 491 |
. . . . . . . . . 10
           
     |
58 | | simplr 528 |
. . . . . . . . . 10
           
    
        |
59 | 31, 57, 58 | mp2and 433 |
. . . . . . . . 9
           
         |
60 | 59 | adantr 276 |
. . . . . . . 8
   
  
                        |
61 | 53, 60 | eqeltrd 2254 |
. . . . . . 7
   
  
                        |
62 | 47 | adantr 276 |
. . . . . . . 8
   
  
                                    |
63 | 59 | adantr 276 |
. . . . . . . . 9
   
  
                        |
64 | 31, 1 | syl 14 |
. . . . . . . . . . . 12
           
         |
65 | | fof 5439 |
. . . . . . . . . . . 12
           |
66 | 64, 65 | syl 14 |
. . . . . . . . . . 11
           
         |
67 | 66, 39 | ffvelcdmd 5653 |
. . . . . . . . . 10
           
         |
68 | 67 | adantr 276 |
. . . . . . . . 9
   
  
                        |
69 | | simpr 110 |
. . . . . . . . 9
   
  
                 
          |
70 | | unsnfi 6918 |
. . . . . . . . 9
                                 |
71 | 63, 68, 69, 70 | syl3anc 1238 |
. . . . . . . 8
   
  
                                |
72 | 62, 71 | eqeltrrd 2255 |
. . . . . . 7
   
  
                        |
73 | | fidcenumlemr.dc |
. . . . . . . . 9
  
DECID   |
74 | 31, 73 | syl 14 |
. . . . . . . 8
           
   

DECID
  |
75 | | simpll 527 |
. . . . . . . 8
           
     |
76 | 74, 64, 75, 57, 67 | fidcenumlemrk 6953 |
. . . . . . 7
           
                       |
77 | 61, 72, 76 | mpjaodan 798 |
. . . . . 6
           
         |
78 | 77 | exp31 364 |
. . . . 5
           
         |
79 | 11, 16, 21, 26, 30, 78 | finds 4600 |
. . . 4
  
        |
80 | 6, 79 | mpcom 36 |
. . 3
 

      |
81 | 4, 80 | mpan2 425 |
. 2
       |
82 | 3, 81 | eqeltrrd 2255 |
1
   |