Step | Hyp | Ref
| Expression |
1 | | heibor.7 |
. . . . . . . 8
          |
2 | | 0nn0 10884 |
. . . . . . . 8
 |
3 | | inss2 3653 |
. . . . . . . . 9
    |
4 | | ffvelrn 6020 |
. . . . . . . . 9
        
          |
5 | 3, 4 | sseldi 3430 |
. . . . . . . 8
        
       |
6 | 1, 2, 5 | sylancl 668 |
. . . . . . 7
       |
7 | | heibor.8 |
. . . . . . . . 9
              |
8 | | fveq2 5865 |
. . . . . . . . . . . 12
           |
9 | | oveq2 6298 |
. . . . . . . . . . . 12
           |
10 | 8, 9 | iuneq12d 4304 |
. . . . . . . . . . 11
           
           |
11 | 10 | eqeq2d 2461 |
. . . . . . . . . 10
 
         
             |
12 | 11 | rspccva 3149 |
. . . . . . . . 9
                          |
13 | 7, 2, 12 | sylancl 668 |
. . . . . . . 8
             |
14 | | eqimss 3484 |
. . . . . . . 8
                       |
15 | 13, 14 | syl 17 |
. . . . . . 7

            |
16 | | heibor.1 |
. . . . . . . . . 10
     |
17 | | heibor.3 |
. . . . . . . . . 10
     
   |
18 | | ovex 6318 |
. . . . . . . . . 10
     |
19 | 16, 17, 18 | heiborlem1 32143 |
. . . . . . . . 9
                             |
20 | | oveq1 6297 |
. . . . . . . . . . 11
           |
21 | 20 | eleq1d 2513 |
. . . . . . . . . 10
     
       |
22 | 21 | cbvrexv 3020 |
. . . . . . . . 9
          
            |
23 | 19, 22 | sylib 200 |
. . . . . . . 8
                             |
24 | 23 | 3expia 1210 |
. . . . . . 7
                               |
25 | 6, 15, 24 | syl2anc 667 |
. . . . . 6
               |
26 | 25 | adantr 467 |
. . . . 5
 
     
             |
27 | | heibor.4 |
. . . . . . . . . 10
    
           |
28 | | vex 3048 |
. . . . . . . . . 10
 |
29 | | c0ex 9637 |
. . . . . . . . . 10
 |
30 | 16, 17, 27, 28, 29 | heiborlem2 32144 |
. . . . . . . . 9
  

   
       |
31 | | heibor.5 |
. . . . . . . . . . . 12
 
                |
32 | | heibor.6 |
. . . . . . . . . . . 12
       |
33 | 16, 17, 27, 31, 32, 1, 7 | heiborlem3 32145 |
. . . . . . . . . . 11
   
                                    |
34 | 33 | ad2antrr 732 |
. . . . . . . . . 10
    
        
                                    |
35 | 32 | ad2antrr 732 |
. . . . . . . . . . . . 13
    
      
                                          |
36 | 1 | ad2antrr 732 |
. . . . . . . . . . . . 13
    
      
                                             |
37 | 7 | ad2antrr 732 |
. . . . . . . . . . . . 13
    
      
                                     
           |
38 | | simprr 766 |
. . . . . . . . . . . . . 14
    
      
                                    
                                    |
39 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
40 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
           |
41 | 40 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
               |
42 | 39, 41 | breq12d 4415 |
. . . . . . . . . . . . . . . 16
             
               |
43 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
           |
44 | 39, 41 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . 18
                               |
45 | 43, 44 | ineq12d 3635 |
. . . . . . . . . . . . . . . . 17
     
                                     |
46 | 45 | eleq1d 2513 |
. . . . . . . . . . . . . . . 16
                     
                       |
47 | 42, 46 | anbi12d 717 |
. . . . . . . . . . . . . . 15
                                                                         |
48 | 47 | cbvralv 3019 |
. . . . . . . . . . . . . 14
 
                                  
                                    |
49 | 38, 48 | sylib 200 |
. . . . . . . . . . . . 13
    
      
                                    
                                    |
50 | | simprl 764 |
. . . . . . . . . . . . 13
    
      
                                        |
51 | | eqeq1 2455 |
. . . . . . . . . . . . . . . 16
     |
52 | | oveq1 6297 |
. . . . . . . . . . . . . . . 16
       |
53 | 51, 52 | ifbieq2d 3906 |
. . . . . . . . . . . . . . 15
                 |
54 | 53 | cbvmptv 4495 |
. . . . . . . . . . . . . 14

        
         |
55 | | seqeq3 12218 |
. . . . . . . . . . . . . 14
          
       
                              |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . . . 13
                             |
57 | | eqid 2451 |
. . . . . . . . . . . . 13
                           
                             |
58 | | simplrl 770 |
. . . . . . . . . . . . 13
    
      
                                      |
59 | | cmetmet 22256 |
. . . . . . . . . . . . . . . . 17
    
      |
60 | | metxmet 21349 |
. . . . . . . . . . . . . . . . 17
    
       |
61 | 16 | mopnuni 21456 |
. . . . . . . . . . . . . . . . 17
         |
62 | 32, 59, 60, 61 | 4syl 19 |
. . . . . . . . . . . . . . . 16
    |
63 | 62 | adantr 467 |
. . . . . . . . . . . . . . 15
 
        |
64 | | simprr 766 |
. . . . . . . . . . . . . . 15
 
         |
65 | 63, 64 | eqtr2d 2486 |
. . . . . . . . . . . . . 14
 
        |
66 | 65 | adantr 467 |
. . . . . . . . . . . . 13
    
      
                                       |
67 | 16, 17, 27, 31, 35, 36, 37, 49, 50, 56, 57, 58, 66 | heiborlem9 32151 |
. . . . . . . . . . . 12
    
      
                                   
  |
68 | 67 | expr 620 |
. . . . . . . . . . 11
    
       
                                 
   |
69 | 68 | exlimdv 1779 |
. . . . . . . . . 10
    
                                           
   |
70 | 34, 69 | mpd 15 |
. . . . . . . . 9
    
     
  |
71 | 30, 70 | sylan2br 479 |
. . . . . . . 8
    
   
   
     
  |
72 | 71 | 3exp2 1227 |
. . . . . . 7
 
          
    
     |
73 | 2, 72 | mpi 20 |
. . . . . 6
 
         
    
    |
74 | 73 | rexlimdv 2877 |
. . . . 5
 
                   |
75 | 26, 74 | syld 45 |
. . . 4
 
     
   |
76 | 75 | pm2.01d 173 |
. . 3
 
    
  |
77 | | elfvdm 5891 |
. . . . . 6
    
  |
78 | | sseq1 3453 |
. . . . . . . . 9
 
     |
79 | 78 | rexbidv 2901 |
. . . . . . . 8
  
 
 
          |
80 | 79 | notbid 296 |
. . . . . . 7
      
     
    |
81 | 80, 17 | elab2g 3187 |
. . . . . 6
 
         |
82 | 32, 77, 81 | 3syl 18 |
. . . . 5
      
    |
83 | 82 | adantr 467 |
. . . 4
 
     
         |
84 | 83 | con2bid 331 |
. . 3
 
               |
85 | 76, 84 | mpbird 236 |
. 2
 
         
   |
86 | 62 | ad2antrr 732 |
. . . . 5
    
          |
87 | 86 | sseq1d 3459 |
. . . 4
    
        
     |
88 | | inss1 3652 |
. . . . . . . . 9
     |
89 | 88 | sseli 3428 |
. . . . . . . 8
       |
90 | 89 | elpwid 3961 |
. . . . . . 7
      |
91 | | simprl 764 |
. . . . . . 7
 
       |
92 | | sstr 3440 |
. . . . . . . 8
 

  |
93 | 92 | unissd 4222 |
. . . . . . 7
 
 
   |
94 | 90, 91, 93 | syl2anr 481 |
. . . . . 6
    
           |
95 | 94 | biantrud 510 |
. . . . 5
    
        
          |
96 | | eqss 3447 |
. . . . 5
 
         |
97 | 95, 96 | syl6bbr 267 |
. . . 4
    
        
      |
98 | 87, 97 | bitrd 257 |
. . 3
    
        
     |
99 | 98 | rexbidva 2898 |
. 2
 
                 
    |
100 | 85, 99 | mpbid 214 |
1
 
              |