Step | Hyp | Ref
| Expression |
1 | | frfnom 7152 |
. . . . . . . 8
                 |
2 | | axdclem2.1 |
. . . . . . . . 9
                 |
3 | 2 | fneq1i 5670 |
. . . . . . . 8

                  |
4 | 1, 3 | mpbir 213 |
. . . . . . 7
 |
5 | 4 | a1i 11 |
. . . . . 6
            
   |
6 | | fveq2 5865 |
. . . . . . . . . . 11

          |
7 | | suceq 5488 |
. . . . . . . . . . . 12

  |
8 | 7 | fveq2d 5869 |
. . . . . . . . . . 11

  
       |
9 | 6, 8 | breq12d 4415 |
. . . . . . . . . 10

          
             |
10 | | fveq2 5865 |
. . . . . . . . . . 11
           |
11 | | suceq 5488 |
. . . . . . . . . . . 12

  |
12 | 11 | fveq2d 5869 |
. . . . . . . . . . 11
           |
13 | 10, 12 | breq12d 4415 |
. . . . . . . . . 10
          
              |
14 | | fveq2 5865 |
. . . . . . . . . . 11
       
   |
15 | | suceq 5488 |
. . . . . . . . . . . 12
   |
16 | 15 | fveq2d 5869 |
. . . . . . . . . . 11
           |
17 | 14, 16 | breq12d 4415 |
. . . . . . . . . 10
                         |
18 | 2 | fveq1i 5866 |
. . . . . . . . . . . . . . . 16
                         |
19 | | vex 3048 |
. . . . . . . . . . . . . . . . 17
 |
20 | | fr0g 7153 |
. . . . . . . . . . . . . . . . 17
                       |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
               
     |
22 | 18, 21 | eqtri 2473 |
. . . . . . . . . . . . . . 15
     |
23 | 22 | breq1i 4409 |
. . . . . . . . . . . . . 14
           |
24 | 23 | biimpri 210 |
. . . . . . . . . . . . 13
           |
25 | 24 | eximi 1707 |
. . . . . . . . . . . 12
              |
26 | | peano1 6712 |
. . . . . . . . . . . . 13
 |
27 | 2 | axdclem 8949 |
. . . . . . . . . . . . 13
                                 |
28 | 26, 27 | mpi 20 |
. . . . . . . . . . . 12
                           
   |
29 | 25, 28 | syl3an3 1303 |
. . . . . . . . . . 11
             
            |
30 | 29 | 3com23 1214 |
. . . . . . . . . 10
            
         
   |
31 | | fvex 5875 |
. . . . . . . . . . . . . . . . 17
     |
32 | | fvex 5875 |
. . . . . . . . . . . . . . . . 17
  
  |
33 | 31, 32 | brelrn 5065 |
. . . . . . . . . . . . . . . 16
                 |
34 | | ssel 3426 |
. . . . . . . . . . . . . . . 16

            |
35 | 33, 34 | syl5 33 |
. . . . . . . . . . . . . . 15

          
       |
36 | 32 | eldm 5032 |
. . . . . . . . . . . . . . 15
               |
37 | 35, 36 | syl6ib 230 |
. . . . . . . . . . . . . 14

          
           |
38 | 37 | ad2antll 735 |
. . . . . . . . . . . . 13
                                   |
39 | | peano2 6713 |
. . . . . . . . . . . . . . . . 17

  |
40 | 2 | axdclem 8949 |
. . . . . . . . . . . . . . . . 17
                  

        
    |
41 | 39, 40 | syl5 33 |
. . . . . . . . . . . . . . . 16
                  

             |
42 | 41 | 3expia 1210 |
. . . . . . . . . . . . . . 15
                                   |
43 | 42 | com3r 82 |
. . . . . . . . . . . . . 14
   
                               |
44 | 43 | imp 431 |
. . . . . . . . . . . . 13
                                   |
45 | 38, 44 | syld 45 |
. . . . . . . . . . . 12
                                     |
46 | 45 | 3adantr2 1168 |
. . . . . . . . . . 11
             
 
                        |
47 | 46 | ex 436 |
. . . . . . . . . 10
   
                    
               |
48 | 9, 13, 17, 30, 47 | finds2 6721 |
. . . . . . . . 9
   
                        |
49 | 48 | com12 32 |
. . . . . . . 8
            
               |
50 | | fvex 5875 |
. . . . . . . . 9
     |
51 | | fvex 5875 |
. . . . . . . . 9
  
  |
52 | 50, 51 | breldm 5039 |
. . . . . . . 8
                 |
53 | 49, 52 | syl6 34 |
. . . . . . 7
            
         |
54 | 53 | ralrimiv 2800 |
. . . . . 6
            
        |
55 | | ffnfv 6049 |
. . . . . 6
              |
56 | 5, 54, 55 | sylanbrc 670 |
. . . . 5
            
       |
57 | | omex 8148 |
. . . . . 6
 |
58 | 57 | a1i 11 |
. . . . 5
            

  |
59 | | vex 3048 |
. . . . . . 7
 |
60 | 59 | dmex 6726 |
. . . . . 6
 |
61 | 60 | a1i 11 |
. . . . 5
            

  |
62 | | fex2 6748 |
. . . . 5
         |
63 | 56, 58, 61, 62 | syl3anc 1268 |
. . . 4
            
   |
64 | 49 | ralrimiv 2800 |
. . . 4
            
              |
65 | | fveq1 5864 |
. . . . . . 7
           |
66 | | fveq1 5864 |
. . . . . . 7
           |
67 | 65, 66 | breq12d 4415 |
. . . . . 6
          
              |
68 | 67 | ralbidv 2827 |
. . . . 5
  
        
               |
69 | 68 | spcegv 3135 |
. . . 4
  
            
        
    |
70 | 63, 64, 69 | sylc 62 |
. . 3
            
                |
71 | 70 | 3exp 1207 |
. 2
 
        
 
                  |
72 | 60 | pwex 4586 |
. . 3

 |
73 | 72 | ac4c 8906 |
. 2
  
        |
74 | 71, 73 | exlimiiv 1777 |
1
       
        
    |