Step | Hyp | Ref
| Expression |
1 | | peano1 6731 |
. . . . . 6
 |
2 | | ne0i 3728 |
. . . . . 6

  |
3 | | brwdomn0 8102 |
. . . . . 6

 * 
       |
4 | 1, 2, 3 | mp2b 10 |
. . . . 5
 *        |
5 | | cnvimass 5194 |
. . . . . . . . . 10
    
 |
6 | | fof 5806 |
. . . . . . . . . . 11
           |
7 | | fdm 5745 |
. . . . . . . . . . 11
       |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
       |
9 | 5, 8 | syl5sseq 3466 |
. . . . . . . . 9
         
  |
10 | | vex 3034 |
. . . . . . . . . . 11
 |
11 | | dmfex 6770 |
. . . . . . . . . . 11
         |
12 | 10, 6, 11 | sylancr 676 |
. . . . . . . . . 10
       |
13 | | elpw2g 4564 |
. . . . . . . . . 10
                |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
                    |
15 | 9, 14 | mpbird 240 |
. . . . . . . 8
             |
16 | | fin1a2lem.b |
. . . . . . . . . . . . . 14
 
   |
17 | 16 | fin1a2lem4 8851 |
. . . . . . . . . . . . 13
     |
18 | | f1cnv 5851 |
. . . . . . . . . . . . 13
            |
19 | | f1ofo 5835 |
. . . . . . . . . . . . 13
             |
20 | 17, 18, 19 | mp2b 10 |
. . . . . . . . . . . 12
      |
21 | | fofun 5807 |
. . . . . . . . . . . 12
     
   |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . 11
  |
23 | 10 | resex 5154 |
. . . . . . . . . . 11
        |
24 | | cofunexg 6776 |
. . . . . . . . . . 11
                       |
25 | 22, 23, 24 | mp2an 686 |
. . . . . . . . . 10
           |
26 | | fofun 5807 |
. . . . . . . . . . . . 13
       |
27 | | fores 5815 |
. . . . . . . . . . . . 13
      
                            |
28 | 26, 5, 27 | sylancl 675 |
. . . . . . . . . . . 12
     
                          |
29 | | f1f 5792 |
. . . . . . . . . . . . . . 15
           |
30 | | frn 5747 |
. . . . . . . . . . . . . . 15
    
  |
31 | 17, 29, 30 | mp2b 10 |
. . . . . . . . . . . . . 14
 |
32 | | foimacnv 5845 |
. . . . . . . . . . . . . 14
     
            |
33 | 31, 32 | mpan2 685 |
. . . . . . . . . . . . 13
                |
34 | | foeq3 5804 |
. . . . . . . . . . . . 13
                                 
                     |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . 12
                              
                   |
36 | 28, 35 | mpbid 215 |
. . . . . . . . . . 11
     
                 |
37 | | foco 5816 |
. . . . . . . . . . 11
                                             |
38 | 20, 36, 37 | sylancr 676 |
. . . . . . . . . 10
      
    
              |
39 | | fowdom 8104 |
. . . . . . . . . 10
           
 
             
   
*        |
40 | 25, 38, 39 | sylancr 676 |
. . . . . . . . 9
     *        |
41 | | cnvexg 6758 |
. . . . . . . . . . . 12
 
  |
42 | | imaexg 6749 |
. . . . . . . . . . . 12
         |
43 | 10, 41, 42 | mp2b 10 |
. . . . . . . . . . 11
      |
44 | | isfin3-2 8815 |
. . . . . . . . . . 11
            FinIII
*         |
45 | 43, 44 | ax-mp 5 |
. . . . . . . . . 10
     
FinIII *        |
46 | 45 | con2bii 339 |
. . . . . . . . 9
 *     
     FinIII |
47 | 40, 46 | sylib 201 |
. . . . . . . 8
          FinIII |
48 | | fin1a2lem.aa |
. . . . . . . . . . . . . . 15
   |
49 | 16, 48 | fin1a2lem6 8853 |
. . . . . . . . . . . . . 14
         |
50 | | f1ocnv 5840 |
. . . . . . . . . . . . . 14
 
     
            |
51 | | f1ofo 5835 |
. . . . . . . . . . . . . 14
      
              |
52 | 49, 50, 51 | mp2b 10 |
. . . . . . . . . . . . 13
 
        |
53 | | foco 5816 |
. . . . . . . . . . . . 13
                               |
54 | 20, 52, 53 | mp2an 686 |
. . . . . . . . . . . 12
   
    
    |
55 | | fofun 5807 |
. . . . . . . . . . . 12
  
 
       
   
    |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . 11
 
 
   |
57 | 10 | resex 5154 |
. . . . . . . . . . 11
          |
58 | | cofunexg 6776 |
. . . . . . . . . . 11
             
        
              |
59 | 56, 57, 58 | mp2an 686 |
. . . . . . . . . 10
  
 
             |
60 | | difss 3549 |
. . . . . . . . . . . . . 14
    
 
 |
61 | 60, 8 | syl5sseqr 3467 |
. . . . . . . . . . . . 13
              |
62 | | fores 5815 |
. . . . . . . . . . . . 13
      
 
  
                               |
63 | 26, 61, 62 | syl2anc 673 |
. . . . . . . . . . . 12
     
                          
     |
64 | | funcnvcnv 5651 |
. . . . . . . . . . . . . . . 16

    |
65 | | imadif 5668 |
. . . . . . . . . . . . . . . 16
  
    
           
    |
66 | 26, 64, 65 | 3syl 18 |
. . . . . . . . . . . . . . 15
                     
    |
67 | 66 | imaeq2d 5174 |
. . . . . . . . . . . . . 14
            
               
     |
68 | | difss 3549 |
. . . . . . . . . . . . . . 15

  |
69 | | foimacnv 5845 |
. . . . . . . . . . . . . . 15
       
                |
70 | 68, 69 | mpan2 685 |
. . . . . . . . . . . . . 14
            
       |
71 | | fimacnv 6027 |
. . . . . . . . . . . . . . . . 17
         
  |
72 | 6, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
         
  |
73 | 72 | difeq1d 3539 |
. . . . . . . . . . . . . . 15
          
               |
74 | 73 | imaeq2d 5174 |
. . . . . . . . . . . . . 14
                 
          
     |
75 | 67, 70, 74 | 3eqtr3rd 2514 |
. . . . . . . . . . . . 13
            
       |
76 | | foeq3 5804 |
. . . . . . . . . . . . 13
        
    
                            
  
                    
    |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . 12
           
                              
              
    |
78 | 63, 77 | mpbid 215 |
. . . . . . . . . . 11
     
                       |
79 | | foco 5816 |
. . . . . . . . . . 11
                                  
 
  
 
                  
      |
80 | 54, 78, 79 | sylancr 676 |
. . . . . . . . . 10
                 
                 |
81 | | fowdom 8104 |
. . . . . . . . . 10
              
   
  
 
                  
     *          |
82 | 59, 80, 81 | sylancr 676 |
. . . . . . . . 9
     * 
        |
83 | | difexg 4545 |
. . . . . . . . . . 11
     
    |
84 | | isfin3-2 8815 |
. . . . . . . . . . 11
                FinIII * 
         |
85 | 12, 83, 84 | 3syl 18 |
. . . . . . . . . 10
             FinIII
*           |
86 | 85 | con2bid 336 |
. . . . . . . . 9
      *       
    
 
FinIII  |
87 | 82, 86 | mpbid 215 |
. . . . . . . 8
            FinIII |
88 | | eleq1 2537 |
. . . . . . . . . . . 12
    
  FinIII
     FinIII  |
89 | | difeq2 3534 |
. . . . . . . . . . . . 13
    
       
    |
90 | 89 | eleq1d 2533 |
. . . . . . . . . . . 12
    
    FinIII
       FinIII  |
91 | 88, 90 | orbi12d 724 |
. . . . . . . . . . 11
    
   FinIII  
FinIII
     
FinIII
       FinIII   |
92 | 91 | notbid 301 |
. . . . . . . . . 10
    
   FinIII   FinIII
      FinIII     
 
FinIII   |
93 | | ioran 498 |
. . . . . . . . . 10
     
 FinIII        FinIII
     
FinIII
    
 
FinIII  |
94 | 92, 93 | syl6bb 269 |
. . . . . . . . 9
    
   FinIII   FinIII
     
FinIII
    
 
FinIII   |
95 | 94 | rspcev 3136 |
. . . . . . . 8
             
FinIII
    
 
FinIII 
 FinIII  
FinIII  |
96 | 15, 47, 87, 95 | syl12anc 1290 |
. . . . . . 7
       FinIII   FinIII  |
97 | | rexnal 2836 |
. . . . . . 7
   FinIII   FinIII    FinIII  
FinIII  |
98 | 96, 97 | sylib 201 |
. . . . . 6
        FinIII  
FinIII  |
99 | 98 | exlimiv 1784 |
. . . . 5
     
   FinIII   FinIII  |
100 | 4, 99 | sylbi 200 |
. . . 4
 *
   FinIII   FinIII  |
101 | 100 | con2i 124 |
. . 3
 
  FinIII   FinIII
*   |
102 | | isfin3-2 8815 |
. . 3
 
FinIII *    |
103 | 101, 102 | syl5ibr 229 |
. 2
  
  FinIII  
FinIII FinIII  |
104 | 103 | imp 436 |
1
     FinIII   FinIII
FinIII |