Step | Hyp | Ref
| Expression |
1 | | isfinite2 7324 |
. . . . . . . 8

  |
2 | | axcclem.1 |
. . . . . . . . . 10
     |
3 | 2 | eleq1i 2467 |
. . . . . . . . 9

      |
4 | | undif1 3663 |
. . . . . . . . . . 11
             |
5 | | snfi 7146 |
. . . . . . . . . . . 12
   |
6 | | unfi 7333 |
. . . . . . . . . . . 12
                   |
7 | 5, 6 | mpan2 653 |
. . . . . . . . . . 11
               |
8 | 4, 7 | syl5eqelr 2489 |
. . . . . . . . . 10
           |
9 | | ssun1 3470 |
. . . . . . . . . 10

    |
10 | | ssfi 7288 |
. . . . . . . . . 10
     
       |
11 | 8, 9, 10 | sylancl 644 |
. . . . . . . . 9
       |
12 | 3, 11 | sylbi 188 |
. . . . . . . 8
   |
13 | | dcomex 8283 |
. . . . . . . . . 10
 |
14 | | isfiniteg 7326 |
. . . . . . . . . 10
 
   |
15 | 13, 14 | ax-mp 8 |
. . . . . . . . 9

  |
16 | | sdomnen 7095 |
. . . . . . . . 9

  |
17 | 15, 16 | sylbi 188 |
. . . . . . . 8
   |
18 | 1, 12, 17 | 3syl 19 |
. . . . . . 7

  |
19 | 18 | con2i 114 |
. . . . . 6

  |
20 | | sdomentr 7200 |
. . . . . . 7
 
   |
21 | 20 | expcom 425 |
. . . . . 6


   |
22 | 19, 21 | mtod 170 |
. . . . 5

  |
23 | | vex 2919 |
. . . . . 6
 |
24 | | difss 3434 |
. . . . . . 7
     |
25 | 2, 24 | eqsstri 3338 |
. . . . . 6
 |
26 | | ssdomg 7112 |
. . . . . 6
     |
27 | 23, 25, 26 | mp2 9 |
. . . . 5
 |
28 | 22, 27 | jctil 524 |
. . . 4

    |
29 | | bren2 7097 |
. . . 4

    |
30 | 28, 29 | sylibr 204 |
. . 3

  |
31 | | entr 7118 |
. . 3
     |
32 | 30, 31 | mpancom 651 |
. 2

  |
33 | | ensym 7115 |
. 2

  |
34 | | bren 7076 |
. . 3

       |
35 | | f1of 5633 |
. . . . . . . 8
    
      |
36 | | peano1 4823 |
. . . . . . . 8
 |
37 | | ffvelrn 5827 |
. . . . . . . 8
             |
38 | 35, 36, 37 | sylancl 644 |
. . . . . . 7
    
      |
39 | | eldifn 3430 |
. . . . . . . . 9
                 |
40 | 39, 2 | eleq2s 2496 |
. . . . . . . 8
    
        |
41 | | fvex 5701 |
. . . . . . . . . . 11
     |
42 | 41 | elsnc 3797 |
. . . . . . . . . 10
      
      |
43 | 42 | notbii 288 |
. . . . . . . . 9
      
      |
44 | | neq0 3598 |
. . . . . . . . 9
            |
45 | 43, 44 | bitr2i 242 |
. . . . . . . 8
     
        |
46 | 40, 45 | sylibr 204 |
. . . . . . 7
    
       |
47 | 38, 46 | syl 16 |
. . . . . 6
    
       |
48 | | elunii 3980 |
. . . . . . . . . . 11
              |
49 | 38, 48 | sylan2 461 |
. . . . . . . . . 10
              |
50 | 35 | ffvelrnda 5829 |
. . . . . . . . . . . . . 14
             |
51 | | difabs 3565 |
. . . . . . . . . . . . . . . . . 18
             |
52 | 2 | difeq1i 3421 |
. . . . . . . . . . . . . . . . . 18
             |
53 | 51, 52, 2 | 3eqtr4i 2434 |
. . . . . . . . . . . . . . . . 17
     |
54 | | pwuni 4355 |
. . . . . . . . . . . . . . . . . 18
   |
55 | | ssdif 3442 |
. . . . . . . . . . . . . . . . . 18
               |
56 | 54, 55 | ax-mp 8 |
. . . . . . . . . . . . . . . . 17
           |
57 | 53, 56 | eqsstr3i 3339 |
. . . . . . . . . . . . . . . 16
       |
58 | 57 | sseli 3304 |
. . . . . . . . . . . . . . 15
                 |
59 | 58 | ralrimivw 2750 |
. . . . . . . . . . . . . 14
                    |
60 | 50, 59 | syl 16 |
. . . . . . . . . . . . 13
                      |
61 | 60 | ralrimiva 2749 |
. . . . . . . . . . . 12
    
                |
62 | | axcclem.2 |
. . . . . . . . . . . . 13
 
       |
63 | 62 | fmpt2 6377 |
. . . . . . . . . . . 12
 
            
               |
64 | 61, 63 | sylib 189 |
. . . . . . . . . . 11
    
               |
65 | 64 | adantl 453 |
. . . . . . . . . 10
                          |
66 | | difexg 4311 |
. . . . . . . . . . . . . 14
 
     |
67 | 23, 66 | ax-mp 8 |
. . . . . . . . . . . . 13
     |
68 | 2, 67 | eqeltri 2474 |
. . . . . . . . . . . 12
 |
69 | 68 | uniex 4664 |
. . . . . . . . . . 11
  |
70 | 69 | axdc4 8292 |
. . . . . . . . . 10
                                             |
71 | 49, 65, 70 | syl2anc 643 |
. . . . . . . . 9
                  
                    |
72 | | 3simpb 955 |
. . . . . . . . . 10
                        
      
               |
73 | 72 | eximi 1582 |
. . . . . . . . 9
                          
       
                |
74 | 71, 73 | syl 16 |
. . . . . . . 8
                  
                |
75 | 74 | ex 424 |
. . . . . . 7
    
    
       
                 |
76 | 75 | exlimiv 1641 |
. . . . . 6
                                    |
77 | 47, 76 | mpcom 34 |
. . . . 5
    
       
                |
78 | | elsn 3789 |
. . . . . . . . . . 11
  
  |
79 | 78 | necon3bbii 2598 |
. . . . . . . . . 10
     |
80 | 2 | eleq2i 2468 |
. . . . . . . . . . . 12


     |
81 | | eldif 3290 |
. . . . . . . . . . . 12
    

     |
82 | 80, 81 | bitri 241 |
. . . . . . . . . . 11


     |
83 | 82 | biimpri 198 |
. . . . . . . . . 10
 
  
  |
84 | 79, 83 | sylan2br 463 |
. . . . . . . . 9
     |
85 | | simpl 444 |
. . . . . . . . . . . 12
             |
86 | | f1ofo 5640 |
. . . . . . . . . . . . . 14
    
      |
87 | | foelrn 5847 |
. . . . . . . . . . . . . 14
     

       |
88 | 86, 87 | sylan 458 |
. . . . . . . . . . . . 13
              |
89 | | suceq 4606 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26

  |
90 | 89 | fveq2d 5691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
91 | | id 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
92 | | fveq2 5687 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
93 | 91, 92 | oveq12d 6058 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
94 | 90, 93 | eleq12d 2472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                             |
95 | 94 | rspcv 3008 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
                           |
96 | 95 | 3ad2ant3 980 |
. . . . . . . . . . . . . . . . . . . . . 22
             
                           |
97 | 96 | imp 419 |
. . . . . . . . . . . . . . . . . . . . 21
       
     
                           |
98 | 97 | 3adant3 977 |
. . . . . . . . . . . . . . . . . . . 20
       
     
                               |
99 | | eqcom 2406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
    
      |
100 | | f1ocnvfv 5975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                    |
101 | 99, 100 | syl5bi 209 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                    |
102 | 101 | 3adant1 975 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                         |
103 | 102 | imp 419 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
                 |
104 | 103 | eqcomd 2409 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
                 |
105 | 104 | 3adant2 976 |
. . . . . . . . . . . . . . . . . . . . . 22
       
     
                        |
106 | | suceq 4606 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
107 | 105, 106 | syl 16 |
. . . . . . . . . . . . . . . . . . . . 21
       
     
                
       |
108 | 107 | fveq2d 5691 |
. . . . . . . . . . . . . . . . . . . 20
       
     
                                |
109 | | simpr 448 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
   |
110 | | ffvelrn 5827 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
        |
111 | | fveq2 5687 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
112 | | eqidd 2405 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               |
113 | | fvex 5701 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
114 | 111, 112,
62, 113 | ovmpt2 6168 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
              |
115 | 109, 110,
114 | syl2anc 643 |
. . . . . . . . . . . . . . . . . . . . . 22
      
               |
116 | 115 | 3adant2 976 |
. . . . . . . . . . . . . . . . . . . . 21
                          |
117 | 116 | 3ad2ant1 978 |
. . . . . . . . . . . . . . . . . . . 20
       
     
                               |
118 | 98, 108, 117 | 3eltr3d 2484 |
. . . . . . . . . . . . . . . . . . 19
       
     
                                |
119 | 35 | ffvelrnda 5829 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
120 | 119 | 3adant1 975 |
. . . . . . . . . . . . . . . . . . . . . 22
                  |
121 | 120 | 3ad2ant1 978 |
. . . . . . . . . . . . . . . . . . . . 21
       
     
                       |
122 | | eleq1 2464 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
123 | 122 | 3ad2ant3 980 |
. . . . . . . . . . . . . . . . . . . . 21
       
     
                         |
124 | 121, 123 | mpbird 224 |
. . . . . . . . . . . . . . . . . . . 20
       
     
                   |
125 | | fveq2 5687 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
126 | | suceq 4606 |
. . . . . . . . . . . . . . . . . . . . . . 23
          
            |
127 | 125, 126 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
128 | 127 | fveq2d 5691 |
. . . . . . . . . . . . . . . . . . . . 21
            
        |
129 | | axcclem.3 |
. . . . . . . . . . . . . . . . . . . . 21
            |
130 | | fvex 5701 |
. . . . . . . . . . . . . . . . . . . . 21
  
       |
131 | 128, 129,
130 | fvmpt 5765 |
. . . . . . . . . . . . . . . . . . . 20
                |
132 | 124, 131 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
       
     
                       
        |
133 | | simp3 959 |
. . . . . . . . . . . . . . . . . . 19
       
     
                       |
134 | 118, 132,
133 | 3eltr4d 2485 |
. . . . . . . . . . . . . . . . . 18
       
     
                       |
135 | 134 | 3exp 1152 |
. . . . . . . . . . . . . . . . 17
             
                
        |
136 | 135 | com3r 75 |
. . . . . . . . . . . . . . . 16
           
      
                    |
137 | 136 | 3expd 1170 |
. . . . . . . . . . . . . . 15
                                         |
138 | 137 | com4r 82 |
. . . . . . . . . . . . . 14
           
    
 
                      |
139 | 138 | rexlimiv 2784 |
. . . . . . . . . . . . 13
                                        |
140 | 88, 139 | syl 16 |
. . . . . . . . . . . 12
                                         |
141 | 85, 140 | mpid 39 |
. . . . . . . . . . 11
                                   |
142 | 141 | imp3a 421 |
. . . . . . . . . 10
             
             
       |
143 | 142 | impancom 428 |
. . . . . . . . 9
                                   |
144 | 84, 143 | syl5 30 |
. . . . . . . 8
                            
        |
145 | 144 | exp3a 426 |
. . . . . . 7
                                     |
146 | 145 | ralrimiv 2748 |
. . . . . 6
                           

       |
147 | | fvrn0 5712 |
. . . . . . . . . . 11
  
           |
148 | 147 | rgenw 2733 |
. . . . . . . . . 10

              |
149 | | eqid 2404 |
. . . . . . . . . . 11
   
                   |
150 | 149 | fmpt 5849 |
. . . . . . . . . 10
 
                                  |
151 | 148, 150 | mpbi 200 |
. . . . . . . . 9
   
                |
152 | | vex 2919 |
. . . . . . . . . . 11
 |
153 | 152 | rnex 5092 |
. . . . . . . . . 10
 |
154 | | p0ex 4346 |
. . . . . . . . . 10
   |
155 | 153, 154 | unex 4666 |
. . . . . . . . 9
     |
156 | | fex2 5562 |
. . . . . . . . 9
                    
                  |
157 | 151, 68, 155, 156 | mp3an 1279 |
. . . . . . . 8
   
        |
158 | 129, 157 | eqeltri 2474 |
. . . . . . 7
 |
159 | | fveq1 5686 |
. . . . . . . . . 10
           |
160 | 159 | eleq1d 2470 |
. . . . . . . . 9
     
       |
161 | 160 | imbi2d 308 |
. . . . . . . 8
       

        |
162 | 161 | ralbidv 2686 |
. . . . . . 7
  
     


        |
163 | 158, 162 | spcev 3003 |
. . . . . 6
 
        
        |
164 | 146, 163 | syl 16 |
. . . . 5
                             
        |
165 | 77, 164 | exlimddv 1645 |
. . . 4
    
  
        |
166 | 165 | exlimiv 1641 |
. . 3
        

       |
167 | 34, 166 | sylbi 188 |
. 2
   
        |
168 | 32, 33, 167 | 3syl 19 |
1

  
        |