Step | Hyp | Ref
| Expression |
1 | | heibor.6 |
. . . 4
       |
2 | | cmetmet 22249 |
. . . 4
    
      |
3 | | metxmet 21342 |
. . . 4
    
       |
4 | 1, 2, 3 | 3syl 18 |
. . 3
        |
5 | | heibor.13 |
. . . 4

  |
6 | | heibor.16 |
. . . 4
   |
7 | 5, 6 | sseldd 3432 |
. . 3
   |
8 | | heibor.15 |
. . 3
   |
9 | | heibor.1 |
. . . 4
     |
10 | 9 | mopni2 21501 |
. . 3
      

           |
11 | 4, 7, 8, 10 | syl3anc 1267 |
. 2
            |
12 | | rphalfcl 11324 |
. . . . . 6

    |
13 | | breq2 4405 |
. . . . . . . 8
           
             |
14 | 13 | rexbidv 2900 |
. . . . . . 7
    
       
        
     |
15 | | heibor.3 |
. . . . . . . 8
     
   |
16 | | heibor.4 |
. . . . . . . 8
    
           |
17 | | heibor.5 |
. . . . . . . 8
 
                |
18 | | heibor.7 |
. . . . . . . 8
          |
19 | | heibor.8 |
. . . . . . . 8
              |
20 | | heibor.9 |
. . . . . . . 8
                                      |
21 | | heibor.10 |
. . . . . . . 8
     |
22 | | heibor.11 |
. . . . . . . 8
               |
23 | | heibor.12 |
. . . . . . . 8
                |
24 | 9, 15, 16, 17, 1, 18, 19, 20, 21, 22, 23 | heiborlem7 32142 |
. . . . . . 7
         
 |
25 | 14, 24 | vtoclri 3123 |
. . . . . 6
  
        
    |
26 | 12, 25 | syl 17 |
. . . . 5

        
    |
27 | 26 | adantl 468 |
. . . 4
 

        
    |
28 | | nnnn0 10873 |
. . . . . . 7
   |
29 | 9, 15, 16, 17, 1, 18, 19, 20, 21, 22 | heiborlem4 32139 |
. . . . . . . 8
 

        |
30 | | fvex 5873 |
. . . . . . . . . 10
     |
31 | | vex 3047 |
. . . . . . . . . 10
 |
32 | 9, 15, 16, 30, 31 | heiborlem2 32137 |
. . . . . . . . 9
      
        
           |
33 | 32 | simp3bi 1024 |
. . . . . . . 8
                 |
34 | 29, 33 | syl 17 |
. . . . . . 7
 

          |
35 | 28, 34 | sylan2 477 |
. . . . . 6
 

          |
36 | 35 | ad2ant2r 752 |
. . . . 5
                           |
37 | 4 | ad2antrr 731 |
. . . . . . . . . 10
                        |
38 | 9, 15, 16, 17, 1, 18, 19, 20, 21, 22, 23 | heiborlem5 32140 |
. . . . . . . . . . . . 13
         |
39 | 38 | ffvelrnda 6020 |
. . . . . . . . . . . 12
 

        |
40 | 39 | ad2ant2r 752 |
. . . . . . . . . . 11
                         |
41 | | xp1st 6820 |
. . . . . . . . . . 11
      
          |
42 | 40, 41 | syl 17 |
. . . . . . . . . 10
                           |
43 | | 2nn 10764 |
. . . . . . . . . . . . . . 15
 |
44 | | nnexpcl 12282 |
. . . . . . . . . . . . . . 15
 
       |
45 | 43, 28, 44 | sylancr 668 |
. . . . . . . . . . . . . 14
       |
46 | 45 | nnrpd 11336 |
. . . . . . . . . . . . 13
       |
47 | 46 | rpreccld 11348 |
. . . . . . . . . . . 12
         |
48 | 47 | ad2antrl 733 |
. . . . . . . . . . 11
                         |
49 | 48 | rpxrd 11339 |
. . . . . . . . . 10
                         |
50 | | xp2nd 6821 |
. . . . . . . . . . . 12
      
          |
51 | 40, 50 | syl 17 |
. . . . . . . . . . 11
                           |
52 | 51 | rpxrd 11339 |
. . . . . . . . . 10
                           |
53 | | 1le3 10823 |
. . . . . . . . . . . . . 14
 |
54 | | elrp 11301 |
. . . . . . . . . . . . . . 15
    
            |
55 | | 1re 9639 |
. . . . . . . . . . . . . . . 16
 |
56 | | 3re 10680 |
. . . . . . . . . . . . . . . 16
 |
57 | | lediv1 10467 |
. . . . . . . . . . . . . . . 16
 
                           |
58 | 55, 56, 57 | mp3an12 1353 |
. . . . . . . . . . . . . . 15
                           |
59 | 54, 58 | sylbi 199 |
. . . . . . . . . . . . . 14
    

               |
60 | 53, 59 | mpbii 215 |
. . . . . . . . . . . . 13
    
              |
61 | 46, 60 | syl 17 |
. . . . . . . . . . . 12
               |
62 | 61 | ad2antrl 733 |
. . . . . . . . . . 11
                               |
63 | | fveq2 5863 |
. . . . . . . . . . . . . . . 16
           |
64 | | oveq2 6296 |
. . . . . . . . . . . . . . . . 17
           |
65 | 64 | oveq2d 6304 |
. . . . . . . . . . . . . . . 16
               |
66 | 63, 65 | opeq12d 4173 |
. . . . . . . . . . . . . . 15
                             |
67 | | opex 4663 |
. . . . . . . . . . . . . . 15
              |
68 | 66, 23, 67 | fvmpt 5946 |
. . . . . . . . . . . . . 14
                    |
69 | 68 | fveq2d 5867 |
. . . . . . . . . . . . 13
                            |
70 | | ovex 6316 |
. . . . . . . . . . . . . 14
       |
71 | 30, 70 | op2nd 6799 |
. . . . . . . . . . . . 13
                
       |
72 | 69, 71 | syl6eq 2500 |
. . . . . . . . . . . 12
                 |
73 | 72 | ad2antrl 733 |
. . . . . . . . . . 11
                                 |
74 | 62, 73 | breqtrrd 4428 |
. . . . . . . . . 10
                                 |
75 | | ssbl 21431 |
. . . . . . . . . 10
       
        
      
                                                                        |
76 | 37, 42, 49, 52, 74, 75 | syl221anc 1278 |
. . . . . . . . 9
                                                                 |
77 | 28 | ad2antrl 733 |
. . . . . . . . . . 11
                   |
78 | | oveq1 6295 |
. . . . . . . . . . . 12
        
                                      |
79 | | oveq2 6296 |
. . . . . . . . . . . . . 14
           |
80 | 79 | oveq2d 6304 |
. . . . . . . . . . . . 13
               |
81 | 80 | oveq2d 6304 |
. . . . . . . . . . . 12
                                               |
82 | | ovex 6316 |
. . . . . . . . . . . 12
                       |
83 | 78, 81, 17, 82 | ovmpt2 6429 |
. . . . . . . . . . 11
         
                                     |
84 | 42, 77, 83 | syl2anc 666 |
. . . . . . . . . 10
                                                     |
85 | 68 | fveq2d 5867 |
. . . . . . . . . . . . 13
                            |
86 | 30, 70 | op1st 6798 |
. . . . . . . . . . . . 13
                
     |
87 | 85, 86 | syl6eq 2500 |
. . . . . . . . . . . 12
               |
88 | 87 | ad2antrl 733 |
. . . . . . . . . . 11
                               |
89 | 88 | oveq1d 6303 |
. . . . . . . . . 10
                                       |
90 | 84, 89 | eqtr3d 2486 |
. . . . . . . . 9
                                                 |
91 | | 1st2nd2 6827 |
. . . . . . . . . . . 12
      
                         |
92 | 40, 91 | syl 17 |
. . . . . . . . . . 11
                                          |
93 | 92 | fveq2d 5867 |
. . . . . . . . . 10
                                                          |
94 | | df-ov 6291 |
. . . . . . . . . 10
                                                    |
95 | 93, 94 | syl6reqr 2503 |
. . . . . . . . 9
                                                       |
96 | 76, 90, 95 | 3sstr3d 3473 |
. . . . . . . 8
                                       |
97 | 9 | mopntop 21448 |
. . . . . . . . . . 11
        |
98 | 37, 97 | syl 17 |
. . . . . . . . . 10
                   |
99 | | blssm 21426 |
. . . . . . . . . . . 12
                                                  |
100 | 37, 42, 52, 99 | syl3anc 1267 |
. . . . . . . . . . 11
                                           |
101 | 9 | mopnuni 21449 |
. . . . . . . . . . . 12
         |
102 | 37, 101 | syl 17 |
. . . . . . . . . . 11
                    |
103 | 100, 95, 102 | 3sstr3d 3473 |
. . . . . . . . . 10
                            
   |
104 | | eqid 2450 |
. . . . . . . . . . 11
   |
105 | 104 | sscls 20064 |
. . . . . . . . . 10
                                                  |
106 | 98, 103, 105 | syl2anc 666 |
. . . . . . . . 9
                            
                      |
107 | 95 | fveq2d 5867 |
. . . . . . . . . . 11
                                                                       |
108 | 12 | ad2antlr 732 |
. . . . . . . . . . . . 13
                     |
109 | 108 | rpxrd 11339 |
. . . . . . . . . . . 12
                     |
110 | | simprr 765 |
. . . . . . . . . . . 12
                        
    |
111 | 9 | blsscls 21515 |
. . . . . . . . . . . 12
       
        
        
 
                                                                |
112 | 37, 42, 52, 109, 110, 111 | syl23anc 1274 |
. . . . . . . . . . 11
                                                                     |
113 | 107, 112 | eqsstr3d 3466 |
. . . . . . . . . 10
                                                         |
114 | | rpre 11305 |
. . . . . . . . . . . 12

  |
115 | 114 | ad2antlr 732 |
. . . . . . . . . . 11
                   |
116 | | heibor.17 |
. . . . . . . . . . . . . . 15
            |
117 | 9, 15, 16, 17, 1, 18, 19, 20, 21, 22, 23 | heiborlem6 32141 |
. . . . . . . . . . . . . . . . 17
                              |
118 | 4, 38, 117, 9 | caublcls 22271 |
. . . . . . . . . . . . . . . 16
 
        
                       |
119 | 118 | 3expia 1209 |
. . . . . . . . . . . . . . 15
 
          
                       |
120 | 116, 119 | mpdan 673 |
. . . . . . . . . . . . . 14
                         |
121 | 120 | imp 431 |
. . . . . . . . . . . . 13
 

                      |
122 | 121 | ad2ant2r 752 |
. . . . . . . . . . . 12
                                       |
123 | 113, 122 | sseldd 3432 |
. . . . . . . . . . 11
                                     |
124 | | blhalf 21413 |
. . . . . . . . . . 11
       
        
                    
                            |
125 | 37, 42, 115, 123, 124 | syl22anc 1268 |
. . . . . . . . . 10
                                             |
126 | 113, 125 | sstrd 3441 |
. . . . . . . . 9
                                               |
127 | 106, 126 | sstrd 3441 |
. . . . . . . 8
                            
          |
128 | 96, 127 | sstrd 3441 |
. . . . . . 7
                                   |
129 | | sstr2 3438 |
. . . . . . 7
                                     |
130 | 128, 129 | syl 17 |
. . . . . 6
                                     |
131 | | unisng 4213 |
. . . . . . . . . . . . 13
   
  |
132 | 6, 131 | syl 17 |
. . . . . . . . . . . 12
      |
133 | 132 | sseq2d 3459 |
. . . . . . . . . . 11
            
           |
134 | 133 | biimpar 488 |
. . . . . . . . . 10
 
                      |
135 | 6 | snssd 4116 |
. . . . . . . . . . . . 13
     |
136 | | snex 4640 |
. . . . . . . . . . . . . 14
 
 |
137 | 136 | elpw 3956 |
. . . . . . . . . . . . 13
        |
138 | 135, 137 | sylibr 216 |
. . . . . . . . . . . 12
      |
139 | | snfi 7647 |
. . . . . . . . . . . . 13
 
 |
140 | 139 | a1i 11 |
. . . . . . . . . . . 12
     |
141 | 138, 140 | elind 3617 |
. . . . . . . . . . 11
        |
142 | | unieq 4205 |
. . . . . . . . . . . . 13
         |
143 | 142 | sseq2d 3459 |
. . . . . . . . . . . 12
                           |
144 | 143 | rspcev 3149 |
. . . . . . . . . . 11
                                   |
145 | 141, 144 | sylan 474 |
. . . . . . . . . 10
 
                            |
146 | 134, 145 | syldan 473 |
. . . . . . . . 9
 
                         |
147 | | ovex 6316 |
. . . . . . . . . . 11
         |
148 | | sseq1 3452 |
. . . . . . . . . . . . 13
         
             |
149 | 148 | rexbidv 2900 |
. . . . . . . . . . . 12
          
 
 
             
    |
150 | 149 | notbid 296 |
. . . . . . . . . . 11
              
                  |
151 | 147, 150,
15 | elab2 3187 |
. . . . . . . . . 10
        
                |
152 | 151 | con2bii 334 |
. . . . . . . . 9
             
           |
153 | 146, 152 | sylib 200 |
. . . . . . . 8
 
                   |
154 | 153 | ex 436 |
. . . . . . 7
                     |
155 | 154 | ad2antrr 731 |
. . . . . 6
                         
           |
156 | 130, 155 | syld 45 |
. . . . 5
                         
           |
157 | 36, 156 | mt2d 121 |
. . . 4
                
          |
158 | 27, 157 | rexlimddv 2882 |
. . 3
 

          |
159 | 158 | nrexdv 2842 |
. 2
            |
160 | 11, 159 | pm2.21dd 178 |
1
   |