Step | Hyp | Ref
| Expression |
1 | | 0nn0 10918 |
. . . . 5
 |
2 | 1 | a1i 11 |
. . . 4
    supp  
  |
3 | | oveq2 6328 |
. . . . . . 7
           |
4 | 3 | sseq2d 3472 |
. . . . . 6
   supp     
 supp 
       |
5 | 4 | ralbidv 2839 |
. . . . 5
  
 supp
       supp
        |
6 | 5 | adantl 472 |
. . . 4
  
  supp
      supp 
   

 supp 
       |
7 | | ral0 3886 |
. . . . . 6
  supp 
     |
8 | | raleq 2999 |
. . . . . 6

 
 supp     

 supp 
       |
9 | 7, 8 | mpbii 216 |
. . . . 5


 supp 
      |
10 | | 0ss 3775 |
. . . . . . 7
     |
11 | | sseq1 3465 |
. . . . . . 7
  supp    supp     
       |
12 | 10, 11 | mpbiri 241 |
. . . . . 6
  supp   supp 
      |
13 | 12 | ralimi 2793 |
. . . . 5
 
 supp    supp
       |
14 | 9, 13 | jaoi 385 |
. . . 4
    supp  

 supp 
      |
15 | 2, 6, 14 | rspcedvd 3167 |
. . 3
    supp  
   supp 
      |
16 | 15 | 2a1d 27 |
. 2
    supp  
 
    
finSupp
   supp 
        |
17 | | simplr 767 |
. . . . 5
   

 supp   
 
   finSupp    
   |
18 | | simpr 467 |
. . . . . 6
   

 supp   
 
   finSupp  
finSupp   |
19 | | ioran 497 |
. . . . . . . . . 10
 
  supp
 
   supp     |
20 | | oveq1 6327 |
. . . . . . . . . . . . . 14
  supp   supp    |
21 | 20 | eqeq1d 2464 |
. . . . . . . . . . . . 13
   supp 
 supp     |
22 | 21 | cbvralv 3031 |
. . . . . . . . . . . 12
 
 supp  
 supp    |
23 | 22 | notbii 302 |
. . . . . . . . . . 11
   supp


 supp    |
24 | 23 | anbi2i 705 |
. . . . . . . . . 10
    supp
 
   supp     |
25 | 19, 24 | bitri 257 |
. . . . . . . . 9
 
  supp
 
   supp     |
26 | | rexnal 2848 |
. . . . . . . . . . 11
   supp


 supp    |
27 | | df-ne 2635 |
. . . . . . . . . . . . . 14
  supp   supp    |
28 | 27 | bicomi 207 |
. . . . . . . . . . . . 13
  supp 
 supp    |
29 | 28 | rexbii 2901 |
. . . . . . . . . . . 12
   supp
   supp
   |
30 | 29 | biimpi 199 |
. . . . . . . . . . 11
   supp


 supp    |
31 | 26, 30 | sylbir 218 |
. . . . . . . . . 10
   supp


 supp    |
32 | 31 | adantl 472 |
. . . . . . . . 9
    supp
  
 supp    |
33 | 25, 32 | sylbi 200 |
. . . . . . . 8
 
  supp
  
 supp    |
34 | 33 | ad2antrr 737 |
. . . . . . 7
   

 supp   
 
   finSupp  
 supp    |
35 | | iunn0 4352 |
. . . . . . 7
   supp    supp
   |
36 | 34, 35 | sylib 201 |
. . . . . 6
   

 supp   
 
   finSupp  
 supp    |
37 | 18, 36 | jca 539 |
. . . . 5
   

 supp   
 
   finSupp   
finSupp 
 supp     |
38 | | oveq1 6327 |
. . . . . . 7
  supp   supp    |
39 | 38 | cbviunv 4331 |
. . . . . 6

 supp  
 supp   |
40 | | eqid 2462 |
. . . . . 6
  
 supp
     
 supp     |
41 | 39, 40 | fsuppmapnn0fiublem 12240 |
. . . . 5
 
      finSupp   supp  
  
 supp
      |
42 | 17, 37, 41 | sylc 62 |
. . . 4
   

 supp   
 
   finSupp      supp
     |
43 | | nfv 1772 |
. . . . . . . . . 10
   |
44 | | nfra1 2781 |
. . . . . . . . . 10
    supp
  |
45 | 43, 44 | nfor 2029 |
. . . . . . . . 9
  
  supp
   |
46 | 45 | nfn 1994 |
. . . . . . . 8
    supp    |
47 | | nfv 1772 |
. . . . . . . 8
    
  |
48 | 46, 47 | nfan 2022 |
. . . . . . 7
   

 supp   
 
   |
49 | | nfra1 2781 |
. . . . . . 7
   finSupp  |
50 | 48, 49 | nfan 2022 |
. . . . . 6
     
 supp    

  
finSupp   |
51 | | nfv 1772 |
. . . . . 6
   
 supp
    |
52 | 50, 51 | nfan 2022 |
. . . . 5
     
  supp
    
   finSupp    
 supp      |
53 | | oveq2 6328 |
. . . . . . 7
   
 supp               supp
      |
54 | 53 | sseq2d 3472 |
. . . . . 6
   
 supp      supp     
 supp 
     
 supp        |
55 | 54 | adantl 472 |
. . . . 5
     
 supp    

  
finSupp      supp
   
  supp     
 supp 
     
 supp        |
56 | 52, 55 | ralbid 2834 |
. . . 4
     
 supp    

  
finSupp      supp
   
 
 supp     

 supp 
     
 supp        |
57 | | rexnal 2848 |
. . . . . . . . . . 11
   supp


 supp    |
58 | | df-ne 2635 |
. . . . . . . . . . . . . 14
  supp   supp    |
59 | 58 | bicomi 207 |
. . . . . . . . . . . . 13
  supp 
 supp    |
60 | 59 | rexbii 2901 |
. . . . . . . . . . . 12
   supp
   supp
   |
61 | 60 | biimpi 199 |
. . . . . . . . . . 11
   supp


 supp    |
62 | 57, 61 | sylbir 218 |
. . . . . . . . . 10
   supp


 supp    |
63 | 62 | adantl 472 |
. . . . . . . . 9
    supp
  
 supp    |
64 | 19, 63 | sylbi 200 |
. . . . . . . 8
 
  supp
  
 supp    |
65 | 64 | ad2antrr 737 |
. . . . . . 7
   

 supp   
 
   finSupp  
 supp    |
66 | | iunn0 4352 |
. . . . . . . 8
   supp    supp
   |
67 | 20 | cbviunv 4331 |
. . . . . . . . 9

 supp  
 supp   |
68 | 67 | neeq1i 2700 |
. . . . . . . 8
 
 supp 
  supp    |
69 | 66, 68 | bitri 257 |
. . . . . . 7
   supp    supp
   |
70 | 65, 69 | sylib 201 |
. . . . . 6
   

 supp   
 
   finSupp  
 supp    |
71 | 18, 70 | jca 539 |
. . . . 5
   

 supp   
 
   finSupp   
finSupp 
 supp     |
72 | 39, 40 | fsuppmapnn0fiub 12241 |
. . . . 5
 
      finSupp   supp  

 supp 
     
 supp        |
73 | 17, 71, 72 | sylc 62 |
. . . 4
   

 supp   
 
   finSupp  
 supp 
     
 supp       |
74 | 42, 56, 73 | rspcedvd 3167 |
. . 3
   

 supp   
 
   finSupp     supp 
      |
75 | 74 | exp31 613 |
. 2
 
  supp
     
  
finSupp
   supp 
        |
76 | 16, 75 | pm2.61i 169 |
1
 
    
finSupp
   supp 
       |