Step | Hyp | Ref
| Expression |
1 | | nfv 1760 |
. . . 4
    
  |
2 | | nfra1 2768 |
. . . . 5
   finSupp  |
3 | | nfv 1760 |
. . . . 5
  |
4 | 2, 3 | nfan 2010 |
. . . 4
    finSupp   |
5 | 1, 4 | nfan 2010 |
. . 3
    

  
finSupp    |
6 | | suppssdm 6924 |
. . . . . . . . . . 11
 supp   |
7 | | ssel2 3426 |
. . . . . . . . . . . . 13
 
       |
8 | | elmapfn 7491 |
. . . . . . . . . . . . 13
  
  |
9 | | fndm 5673 |
. . . . . . . . . . . . . 14

  |
10 | | eqimss 3483 |
. . . . . . . . . . . . . 14

  |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . 13

  |
12 | 7, 8, 11 | 3syl 18 |
. . . . . . . . . . . 12
 
     |
13 | 12 | 3ad2antl1 1169 |
. . . . . . . . . . 11
    
    |
14 | 6, 13 | syl5ss 3442 |
. . . . . . . . . 10
    
   supp    |
15 | 14 | sseld 3430 |
. . . . . . . . 9
    
    supp     |
16 | 15 | adantlr 720 |
. . . . . . . 8
    

  
finSupp  
   supp 
   |
17 | 16 | imp 431 |
. . . . . . 7
      
  
finSupp     supp  
  |
18 | | fsuppmapnn0fiub.u |
. . . . . . . . . 10
  supp
  |
19 | | fsuppmapnn0fiub.s |
. . . . . . . . . 10
   
 |
20 | 18, 19 | fsuppmapnn0fiublem 12199 |
. . . . . . . . 9
 
      finSupp     |
21 | 20 | imp 431 |
. . . . . . . 8
    
  
finSupp     |
22 | 21 | ad2antrr 731 |
. . . . . . 7
      
  
finSupp     supp  
  |
23 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
 
  
  |
24 | 23 | ex 436 |
. . . . . . . . . . . . . . . . . 18
  

   |
25 | 24 | 3ad2ant1 1028 |
. . . . . . . . . . . . . . . . 17
 
   
   |
26 | 25 | adantr 467 |
. . . . . . . . . . . . . . . 16
    
  
finSupp   
   |
27 | 26 | imp 431 |
. . . . . . . . . . . . . . 15
    

  
finSupp  
   |
28 | | nn0ssre 10870 |
. . . . . . . . . . . . . . 15
 |
29 | 27, 28 | syl6eqss 3481 |
. . . . . . . . . . . . . 14
    

  
finSupp  
   |
30 | 6, 29 | syl5ss 3442 |
. . . . . . . . . . . . 13
    

  
finSupp  
  supp    |
31 | 30 | ex 436 |
. . . . . . . . . . . 12
    
  
finSupp     supp     |
32 | 5, 31 | ralrimi 2787 |
. . . . . . . . . . 11
    
  
finSupp   
 supp 
  |
33 | 32 | ad2antrr 731 |
. . . . . . . . . 10
      
  
finSupp     supp  

 supp 
  |
34 | | iunss 4318 |
. . . . . . . . . 10
 
 supp    supp    |
35 | 33, 34 | sylibr 216 |
. . . . . . . . 9
      
  
finSupp     supp  
  supp 
  |
36 | 18, 35 | syl5eqss 3475 |
. . . . . . . 8
      
  
finSupp     supp  
  |
37 | | simp2 1008 |
. . . . . . . . . . . 12
 
     |
38 | | id 22 |
. . . . . . . . . . . . . . 15
 finSupp finSupp
  |
39 | 38 | fsuppimpd 7887 |
. . . . . . . . . . . . . 14
 finSupp  supp    |
40 | 39 | ralimi 2780 |
. . . . . . . . . . . . 13
 
finSupp   supp
   |
41 | 40 | adantr 467 |
. . . . . . . . . . . 12
   finSupp 

 supp    |
42 | 37, 41 | anim12i 569 |
. . . . . . . . . . 11
    
  
finSupp   

 supp     |
43 | 42 | ad2antrr 731 |
. . . . . . . . . 10
      
  
finSupp     supp  
 
 supp     |
44 | | iunfi 7859 |
. . . . . . . . . 10
    supp   
 supp    |
45 | 43, 44 | syl 17 |
. . . . . . . . 9
      
  
finSupp     supp  
  supp    |
46 | 18, 45 | syl5eqel 2532 |
. . . . . . . 8
      
  
finSupp     supp  
  |
47 | | simpr 463 |
. . . . . . . . . . . 12
    

  
finSupp  
   |
48 | | oveq1 6295 |
. . . . . . . . . . . . . 14
  supp   supp    |
49 | 48 | eleq2d 2513 |
. . . . . . . . . . . . 13
   supp 
 supp
    |
50 | 49 | adantl 468 |
. . . . . . . . . . . 12
      
  
finSupp       supp 
 supp
    |
51 | 47, 50 | rspcedv 3153 |
. . . . . . . . . . 11
    

  
finSupp  
   supp  
 supp     |
52 | 51 | imp 431 |
. . . . . . . . . 10
      
  
finSupp     supp  

 supp
   |
53 | | oveq1 6295 |
. . . . . . . . . . . 12
  supp   supp    |
54 | 53 | eleq2d 2513 |
. . . . . . . . . . 11
   supp 
 supp
    |
55 | 54 | cbvrexv 3019 |
. . . . . . . . . 10
   supp  
 supp    |
56 | 52, 55 | sylibr 216 |
. . . . . . . . 9
      
  
finSupp     supp  

 supp
   |
57 | 18 | eleq2i 2520 |
. . . . . . . . . 10

  supp    |
58 | | eliun 4282 |
. . . . . . . . . 10
   supp  
 supp    |
59 | 57, 58 | bitri 253 |
. . . . . . . . 9


 supp
   |
60 | 56, 59 | sylibr 216 |
. . . . . . . 8
      
  
finSupp     supp  
  |
61 | 19 | a1i 11 |
. . . . . . . 8
      
  
finSupp     supp  
      |
62 | 36, 46, 60, 61 | supfirege 10595 |
. . . . . . 7
      
  
finSupp     supp  
  |
63 | | elfz2nn0 11882 |
. . . . . . 7
    

   |
64 | 17, 22, 62, 63 | syl3anbrc 1191 |
. . . . . 6
      
  
finSupp     supp  
      |
65 | 64 | ex 436 |
. . . . 5
    

  
finSupp  
   supp 
       |
66 | 65 | ssrdv 3437 |
. . . 4
    

  
finSupp  
  supp        |
67 | 66 | ex 436 |
. . 3
    
  
finSupp     supp         |
68 | 5, 67 | ralrimi 2787 |
. 2
    
  
finSupp   
 supp 
      |
69 | 68 | ex 436 |
1
 
      finSupp  
 supp 
       |