Step | Hyp | Ref
| Expression |
1 | | fin23lem.e |
. 2
  
                |
2 | | eqif 3931 |
. . 3
                        
               |
3 | 2 | biimpi 199 |
. 2
                  
 
   
               |
4 | | simpr 467 |
. . . . . . . . . . 11
     |
5 | | fin23lem.d |
. . . . . . . . . . . 12
             |
6 | 5 | funmpt2 5638 |
. . . . . . . . . . 11
 |
7 | | funco 5639 |
. . . . . . . . . . 11
  
    |
8 | 4, 6, 7 | sylancl 673 |
. . . . . . . . . 10
       |
9 | | elunirn 6181 |
. . . . . . . . . 10
  
   
             |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
                    |
11 | | dmcoss 5113 |
. . . . . . . . . . . 12
 
 |
12 | 11 | sseli 3440 |
. . . . . . . . . . 11
     |
13 | | fvco 5964 |
. . . . . . . . . . . . . . . 16
                   |
14 | 6, 13 | mpan 681 |
. . . . . . . . . . . . . . 15
                 |
15 | 14 | adantl 472 |
. . . . . . . . . . . . . 14
   
                 |
16 | 15 | eleq2d 2525 |
. . . . . . . . . . . . 13
   
                   |
17 | | incom 3637 |
. . . . . . . . . . . . . . . 16
                       |
18 | | difss 3572 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
19 | | ominf 7810 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
20 | | fin23lem.b |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
        |
21 | | ssrab2 3526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
      |
22 | 20, 21 | eqsstri 3474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 |
23 | | undif 3860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

      |
24 | 22, 23 | mpbi 213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     |
25 | | unfi 7864 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           |
26 | 24, 25 | syl5eqelr 2545 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
27 | 26 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
28 | 19, 27 | mtoi 183 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
29 | 28 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

    |
30 | 5 | fin23lem22 8783 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
           |
31 | 18, 29, 30 | sylancr 674 |
. . . . . . . . . . . . . . . . . . . . . 22
   
         |
32 | | f1of 5837 |
. . . . . . . . . . . . . . . . . . . . . 22
      
        |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
   
         |
34 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
   
   |
35 | | fdm 5756 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
36 | 33, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
   

  |
37 | 34, 36 | eleqtrd 2542 |
. . . . . . . . . . . . . . . . . . . . 21
   
   |
38 | 33, 37 | ffvelrnd 6046 |
. . . . . . . . . . . . . . . . . . . 20
   
         |
39 | 38 | eldifbd 3429 |
. . . . . . . . . . . . . . . . . . 19
   

      |
40 | 20 | eleq2i 2532 |
. . . . . . . . . . . . . . . . . . 19
    
             |
41 | 39, 40 | sylnib 310 |
. . . . . . . . . . . . . . . . . 18
   

             |
42 | 38 | eldifad 3428 |
. . . . . . . . . . . . . . . . . . 19
   
       |
43 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
44 | 43 | sseq2d 3472 |
. . . . . . . . . . . . . . . . . . . 20
           
           |
45 | 44 | elrab3 3209 |
. . . . . . . . . . . . . . . . . . 19
           
    
            |
46 | 42, 45 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   
            
            |
47 | 41, 46 | mtbid 306 |
. . . . . . . . . . . . . . . . 17
   

           |
48 | | fin23lem.a |
. . . . . . . . . . . . . . . . . . 19
seq𝜔  
                      |
49 | 48 | fin23lem20 8793 |
. . . . . . . . . . . . . . . . . 18
                             |
50 | 42, 49 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
            
            |
51 | | orel1 388 |
. . . . . . . . . . . . . . . . 17
 
                    
         
 
            |
52 | 47, 50, 51 | sylc 62 |
. . . . . . . . . . . . . . . 16
   
              |
53 | 17, 52 | syl5eq 2508 |
. . . . . . . . . . . . . . 15
   
              |
54 | | disj 3817 |
. . . . . . . . . . . . . . 15
         
 
         
  |
55 | 53, 54 | sylib 201 |
. . . . . . . . . . . . . 14
   
             |
56 | | rsp 2766 |
. . . . . . . . . . . . . 14
 
                 
    |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . 13
   
         
    |
58 | 16, 57 | sylbid 223 |
. . . . . . . . . . . 12
   
       
    |
59 | 58 | ex 440 |
. . . . . . . . . . 11
                |
60 | 12, 59 | syl5 33 |
. . . . . . . . . 10
            
     |
61 | 60 | rexlimdv 2889 |
. . . . . . . . 9
    
             |
62 | 10, 61 | sylbid 223 |
. . . . . . . 8
      
    |
63 | 62 | ralrimiv 2812 |
. . . . . . 7
          |
64 | | disj 3817 |
. . . . . . 7
           
  |
65 | 63, 64 | sylibr 217 |
. . . . . 6
           |
66 | | rneq 5079 |
. . . . . . . . 9
       |
67 | 66 | unieqd 4222 |
. . . . . . . 8
         |
68 | 67 | ineq1d 3645 |
. . . . . . 7
               |
69 | 68 | eqeq1d 2464 |
. . . . . 6
       
   
     |
70 | 65, 69 | syl5ibr 229 |
. . . . 5
             |
71 | 70 | expd 442 |
. . . 4
   

        |
72 | 71 | impcom 436 |
. . 3
 
   
       |
73 | | rneq 5079 |
. . . . . . . 8
           
             |
74 | 73 | unieqd 4222 |
. . . . . . 7
             
      
      |
75 | 74 | ineq1d 3645 |
. . . . . 6
                                 |
76 | | rncoss 5114 |
. . . . . . . 8
                     |
77 | 76 | unissi 4235 |
. . . . . . 7
                       |
78 | | disj 3817 |
. . . . . . . 8
             
           
  |
79 | | eluniab 4223 |
. . . . . . . . . 10
        
  
        
     |
80 | | eleq2 2529 |
. . . . . . . . . . . . . 14
                   |
81 | | eldifn 3568 |
. . . . . . . . . . . . . 14
       
   |
82 | 80, 81 | syl6bi 236 |
. . . . . . . . . . . . 13
        
    |
83 | 82 | rexlimivw 2888 |
. . . . . . . . . . . 12
         
    |
84 | 83 | impcom 436 |
. . . . . . . . . . 11
          
   |
85 | 84 | exlimiv 1787 |
. . . . . . . . . 10
    
       
   |
86 | 79, 85 | sylbi 200 |
. . . . . . . . 9
        
  
   |
87 | | eqid 2462 |
. . . . . . . . . . 11
                   |
88 | 87 | rnmpt 5099 |
. . . . . . . . . 10
     
    
         |
89 | 88 | unieqi 4221 |
. . . . . . . . 9
            
         |
90 | 86, 89 | eleq2s 2558 |
. . . . . . . 8
       
  
   |
91 | 78, 90 | mprgbir 2764 |
. . . . . . 7
              |
92 | | ssdisj 3826 |
. . . . . . 7
         
   
      
                                  |
93 | 77, 91, 92 | mp2an 683 |
. . . . . 6
                |
94 | 75, 93 | syl6eq 2512 |
. . . . 5
                  |
95 | 94 | a1d 26 |
. . . 4
                    |
96 | 95 | adantl 472 |
. . 3
        
     
       |
97 | 72, 96 | jaoi 385 |
. 2
                   
        |
98 | 1, 3, 97 | mp2b 10 |
1

      |