Step | Hyp | Ref
| Expression |
1 | | elmapi 7524 |
. . . 4
           |
2 | | compss.a |
. . . . . 6
      |
3 | 2 | isf34lem7 8840 |
. . . . 5
 
FinIII
     
            |
4 | 3 | 3expia 1217 |
. . . 4
 
FinIII
                    |
5 | 1, 4 | sylan2 481 |
. . 3
 
FinIII
     
   
        |
6 | 5 | ralrimiva 2814 |
. 2
 FinIII                    |
7 | | elmapex 7523 |
. . . . . . . . . . 11
     
   |
8 | 7 | simpld 465 |
. . . . . . . . . 10
    
  |
9 | | pwexb 6634 |
. . . . . . . . . 10

   |
10 | 8, 9 | sylibr 217 |
. . . . . . . . 9
      |
11 | 2 | isf34lem2 8834 |
. . . . . . . . 9
         |
12 | 10, 11 | syl 17 |
. . . . . . . 8
            |
13 | | elmapi 7524 |
. . . . . . . 8
           |
14 | | fco 5766 |
. . . . . . . 8
       
               |
15 | 12, 13, 14 | syl2anc 671 |
. . . . . . 7
    
        |
16 | | elmapg 7516 |
. . . . . . . 8
                    |
17 | 7, 16 | syl 17 |
. . . . . . 7
                    |
18 | 15, 17 | mpbird 240 |
. . . . . 6
    
      |
19 | | fveq1 5891 |
. . . . . . . . . 10
               |
20 | | fveq1 5891 |
. . . . . . . . . 10
               |
21 | 19, 20 | sseq12d 3473 |
. . . . . . . . 9
       
   
 
             |
22 | 21 | ralbidv 2839 |
. . . . . . . 8
    
   
   
                |
23 | | rneq 5082 |
. . . . . . . . . . 11
  
    |
24 | | rnco2 5365 |
. . . . . . . . . . 11

      |
25 | 23, 24 | syl6eq 2512 |
. . . . . . . . . 10
  
      |
26 | 25 | unieqd 4222 |
. . . . . . . . 9
   
       |
27 | 26, 25 | eleq12d 2534 |
. . . . . . . 8
                 |
28 | 22, 27 | imbi12d 326 |
. . . . . . 7
               
 
                         |
29 | 28 | rspccv 3159 |
. . . . . 6
 
         
                                       |
30 | 18, 29 | syl5 33 |
. . . . 5
 
         
                                     |
31 | | sscon 3579 |
. . . . . . . . 9
    
          
       |
32 | 10 | adantr 471 |
. . . . . . . . . . 11
    
   |
33 | 13 | ffvelrnda 6050 |
. . . . . . . . . . . 12
    
        |
34 | 33 | elpwid 3973 |
. . . . . . . . . . 11
    
       |
35 | 2 | isf34lem1 8833 |
. . . . . . . . . . 11
     
                 |
36 | 32, 34, 35 | syl2anc 671 |
. . . . . . . . . 10
    
                 |
37 | | peano2 6745 |
. . . . . . . . . . . . 13

  |
38 | | ffvelrn 6048 |
. . . . . . . . . . . . 13
               |
39 | 13, 37, 38 | syl2an 484 |
. . . . . . . . . . . 12
    
        |
40 | 39 | elpwid 3973 |
. . . . . . . . . . 11
    
       |
41 | 2 | isf34lem1 8833 |
. . . . . . . . . . 11
      
                |
42 | 32, 40, 41 | syl2anc 671 |
. . . . . . . . . 10
    
                 |
43 | 36, 42 | sseq12d 3473 |
. . . . . . . . 9
    
               
                 |
44 | 31, 43 | syl5ibr 229 |
. . . . . . . 8
    
    
    
                   |
45 | | fvco3 5970 |
. . . . . . . . . 10
      
                 |
46 | 13, 45 | sylan 478 |
. . . . . . . . 9
    
                 |
47 | | fvco3 5970 |
. . . . . . . . . 10
                   
    |
48 | 13, 37, 47 | syl2an 484 |
. . . . . . . . 9
    
            
    |
49 | 46, 48 | sseq12d 3473 |
. . . . . . . 8
    
             
                   |
50 | 44, 49 | sylibrd 242 |
. . . . . . 7
    
    
    
 
             |
51 | 50 | ralimdva 2808 |
. . . . . 6
     
              
 
       |
52 | | ffn 5755 |
. . . . . . . . 9
          |
53 | 12, 52 | syl 17 |
. . . . . . . 8
       |
54 | | imassrn 5201 |
. . . . . . . . 9
  
  |
55 | | frn 5762 |
. . . . . . . . . 10
          |
56 | 12, 55 | syl 17 |
. . . . . . . . 9
       |
57 | 54, 56 | syl5ss 3455 |
. . . . . . . 8
           |
58 | | fnfvima 6173 |
. . . . . . . . 9
           
                    
    |
59 | 58 | 3expia 1217 |
. . . . . . . 8
                  
                    |
60 | 53, 57, 59 | syl2anc 671 |
. . . . . . 7
             
                    |
61 | | incom 3637 |
. . . . . . . . . . . . 13

    |
62 | | frn 5762 |
. . . . . . . . . . . . . . . 16
         |
63 | 13, 62 | syl 17 |
. . . . . . . . . . . . . . 15
       |
64 | | fdm 5760 |
. . . . . . . . . . . . . . . 16
          |
65 | 12, 64 | syl 17 |
. . . . . . . . . . . . . . 15
       |
66 | 63, 65 | sseqtr4d 3481 |
. . . . . . . . . . . . . 14
      |
67 | | df-ss 3430 |
. . . . . . . . . . . . . 14


   |
68 | 66, 67 | sylib 201 |
. . . . . . . . . . . . 13
    
   |
69 | 61, 68 | syl5eq 2508 |
. . . . . . . . . . . 12
        |
70 | | fdm 5760 |
. . . . . . . . . . . . . . 15
        |
71 | 13, 70 | syl 17 |
. . . . . . . . . . . . . 14
   
  |
72 | | peano1 6744 |
. . . . . . . . . . . . . . 15
 |
73 | | ne0i 3749 |
. . . . . . . . . . . . . . 15

  |
74 | 72, 73 | mp1i 13 |
. . . . . . . . . . . . . 14
      |
75 | 71, 74 | eqnetrd 2703 |
. . . . . . . . . . . . 13
      |
76 | | dm0rn0 5073 |
. . . . . . . . . . . . . 14

  |
77 | 76 | necon3bii 2688 |
. . . . . . . . . . . . 13

  |
78 | 75, 77 | sylib 201 |
. . . . . . . . . . . 12
      |
79 | 69, 78 | eqnetrd 2703 |
. . . . . . . . . . 11
        |
80 | | imadisj 5209 |
. . . . . . . . . . . 12
    

   |
81 | 80 | necon3bii 2688 |
. . . . . . . . . . 11
    

   |
82 | 79, 81 | sylibr 217 |
. . . . . . . . . 10
          |
83 | 2 | isf34lem4 8838 |
. . . . . . . . . 10
                                  |
84 | 10, 57, 82, 83 | syl12anc 1274 |
. . . . . . . . 9
          
             |
85 | 2 | isf34lem3 8836 |
. . . . . . . . . . 11
 
 
          |
86 | 10, 63, 85 | syl2anc 671 |
. . . . . . . . . 10
              |
87 | 86 | inteqd 4253 |
. . . . . . . . 9
             
  |
88 | 84, 87 | eqtrd 2496 |
. . . . . . . 8
          
     |
89 | 88, 86 | eleq12d 2534 |
. . . . . . 7
                   
      |
90 | 60, 89 | sylibd 222 |
. . . . . 6
             
    |
91 | 51, 90 | imim12d 77 |
. . . . 5
                              
             |
92 | 30, 91 | sylcom 30 |
. . . 4
 
         
                         |
93 | 92 | ralrimiv 2812 |
. . 3
 
         
                         |
94 | | isfin3-3 8829 |
. . 3
 
FinIII                     |
95 | 93, 94 | syl5ibr 229 |
. 2
  
 
             
FinIII  |
96 | 6, 95 | impbid2 209 |
1
 
FinIII                     |