Step | Hyp | Ref
| Expression |
1 | | bcthlem.4 |
. . . 4
       |
2 | | cmetmet 22249 |
. . . . . . 7
    
      |
3 | 1, 2 | syl 17 |
. . . . . 6
       |
4 | | metxmet 21342 |
. . . . . 6
    
       |
5 | 3, 4 | syl 17 |
. . . . 5
        |
6 | | bcthlem.9 |
. . . . 5
         |
7 | | bcth.2 |
. . . . . 6
     |
8 | | bcthlem.5 |
. . . . . 6
 
       
                                       |
9 | | bcthlem.6 |
. . . . . 6
           |
10 | | bcthlem.7 |
. . . . . 6
   |
11 | | bcthlem.8 |
. . . . . 6
   |
12 | | bcthlem.10 |
. . . . . 6
          |
13 | | bcthlem.11 |
. . . . . 6
                  |
14 | 7, 1, 8, 9, 10, 11, 6, 12, 13 | bcthlem2 22286 |
. . . . 5
                              |
15 | | elrp 11301 |
. . . . . . . . 9

    |
16 | | nnrecl 10864 |
. . . . . . . . 9
   
 
  |
17 | 15, 16 | sylbi 199 |
. . . . . . . 8

     |
18 | 17 | adantl 468 |
. . . . . . 7
 

     |
19 | | peano2nn 10618 |
. . . . . . . . . 10
     |
20 | 19 | adantl 468 |
. . . . . . . . 9
         |
21 | | oveq1 6295 |
. . . . . . . . . . . . . . . . 17
       |
22 | 21 | fveq2d 5867 |
. . . . . . . . . . . . . . . 16
          
    |
23 | | id 22 |
. . . . . . . . . . . . . . . . 17
   |
24 | | fveq2 5863 |
. . . . . . . . . . . . . . . . 17
           |
25 | 23, 24 | oveq12d 6306 |
. . . . . . . . . . . . . . . 16
                   |
26 | 22, 25 | eleq12d 2522 |
. . . . . . . . . . . . . . 15
               
                 |
27 | 26 | rspccva 3148 |
. . . . . . . . . . . . . 14
                
                 |
28 | 13, 27 | sylan 474 |
. . . . . . . . . . . . 13
 

                |
29 | 6 | ffvelrnda 6020 |
. . . . . . . . . . . . . 14
 

        |
30 | 7, 1, 8 | bcthlem1 22285 |
. . . . . . . . . . . . . . 15
 
             
              
                                                  
         |
31 | 30 | expr 619 |
. . . . . . . . . . . . . 14
 

      
              
                                                       
          |
32 | 29, 31 | mpd 15 |
. . . . . . . . . . . . 13
 

              
                                                       
         |
33 | 28, 32 | mpbid 214 |
. . . . . . . . . . . 12
 

                                                       
        |
34 | 33 | simp2d 1020 |
. . . . . . . . . . 11
 

              |
35 | 34 | adantlr 720 |
. . . . . . . . . 10
           
       |
36 | 33 | simp1d 1019 |
. . . . . . . . . . . . . 14
 

          |
37 | | xp2nd 6821 |
. . . . . . . . . . . . . 14
        
            |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . 13
 

            |
39 | 38 | rpred 11338 |
. . . . . . . . . . . 12
 

            |
40 | 39 | adantlr 720 |
. . . . . . . . . . 11
           
     |
41 | | nnrecre 10643 |
. . . . . . . . . . . 12
     |
42 | 41 | adantl 468 |
. . . . . . . . . . 11
         |
43 | | rpre 11305 |
. . . . . . . . . . . 12

  |
44 | 43 | ad2antlr 732 |
. . . . . . . . . . 11
       |
45 | | lttr 9707 |
. . . . . . . . . . 11
             
                 
             |
46 | 40, 42, 44, 45 | syl3anc 1267 |
. . . . . . . . . 10
                    
              |
47 | 35, 46 | mpand 680 |
. . . . . . . . 9
       
             |
48 | | fveq2 5863 |
. . . . . . . . . . . 12
          
    |
49 | 48 | fveq2d 5867 |
. . . . . . . . . . 11
                       |
50 | 49 | breq1d 4411 |
. . . . . . . . . 10
           
             |
51 | 50 | rspcev 3149 |
. . . . . . . . 9
               
          |
52 | 20, 47, 51 | syl6an 548 |
. . . . . . . 8
       
            |
53 | 52 | rexlimdva 2878 |
. . . . . . 7
 

 
          
   |
54 | 18, 53 | mpd 15 |
. . . . . 6
 

        
  |
55 | 54 | ralrimiva 2801 |
. . . . 5
             |
56 | 5, 6, 14, 55 | caubl 22270 |
. . . 4
         |
57 | 7 | cmetcau 22252 |
. . . 4
                      |
58 | 1, 56, 57 | syl2anc 666 |
. . 3
          |
59 | | fo1st 6810 |
. . . . . 6
     |
60 | | fofun 5792 |
. . . . . 6
       |
61 | 59, 60 | ax-mp 5 |
. . . . 5
 |
62 | | vex 3047 |
. . . . 5
 |
63 | | cofunexg 6754 |
. . . . 5
 
     |
64 | 61, 62, 63 | mp2an 677 |
. . . 4
   |
65 | 64 | eldm 5031 |
. . 3
       
  
          |
66 | 58, 65 | sylib 200 |
. 2
              |
67 | | 1nn 10617 |
. . . . . 6
 |
68 | 7, 1, 8, 9, 10, 11, 6, 12, 13 | bcthlem3 22287 |
. . . . . 6
 
        
               |
69 | 67, 68 | mp3an3 1352 |
. . . . 5
 
                        |
70 | 12 | fveq2d 5867 |
. . . . . . 7
                          |
71 | | df-ov 6291 |
. . . . . . 7
                    |
72 | 70, 71 | syl6eqr 2502 |
. . . . . 6
                       |
73 | 72 | adantr 467 |
. . . . 5
 
                                |
74 | 69, 73 | eleqtrd 2530 |
. . . 4
 
                    |
75 | 7 | mopntop 21448 |
. . . . . . . . . . . . . 14
        |
76 | 5, 75 | syl 17 |
. . . . . . . . . . . . 13
   |
77 | 76 | adantr 467 |
. . . . . . . . . . . 12
 

  |
78 | 5 | adantr 467 |
. . . . . . . . . . . . . 14
 

       |
79 | | xp1st 6820 |
. . . . . . . . . . . . . . 15
        
            |
80 | 36, 79 | syl 17 |
. . . . . . . . . . . . . 14
 

            |
81 | 38 | rpxrd 11339 |
. . . . . . . . . . . . . 14
 

            |
82 | | blssm 21426 |
. . . . . . . . . . . . . 14
                                                          |
83 | 78, 80, 81, 82 | syl3anc 1267 |
. . . . . . . . . . . . 13
 

                              |
84 | | 1st2nd2 6827 |
. . . . . . . . . . . . . . . 16
        
                               |
85 | 36, 84 | syl 17 |
. . . . . . . . . . . . . . 15
 

                               |
86 | 85 | fveq2d 5867 |
. . . . . . . . . . . . . 14
 

                                               |
87 | | df-ov 6291 |
. . . . . . . . . . . . . 14
                                                            |
88 | 86, 87 | syl6reqr 2503 |
. . . . . . . . . . . . 13
 

                                            |
89 | 7 | mopnuni 21449 |
. . . . . . . . . . . . . . 15
         |
90 | 5, 89 | syl 17 |
. . . . . . . . . . . . . 14
    |
91 | 90 | adantr 467 |
. . . . . . . . . . . . 13
 

   |
92 | 83, 88, 91 | 3sstr3d 3473 |
. . . . . . . . . . . 12
 

                 |
93 | | eqid 2450 |
. . . . . . . . . . . . 13
   |
94 | 93 | sscls 20064 |
. . . . . . . . . . . 12
                                                        |
95 | 77, 92, 94 | syl2anc 666 |
. . . . . . . . . . 11
 

                                      |
96 | 33 | simp3d 1021 |
. . . . . . . . . . 11
 

                                          |
97 | 95, 96 | sstrd 3441 |
. . . . . . . . . 10
 

                                  |
98 | 97 | 3adant2 1026 |
. . . . . . . . 9
 
        
                           
       |
99 | 7, 1, 8, 9, 10, 11, 6, 12, 13 | bcthlem3 22287 |
. . . . . . . . . 10
 
         
                  |
100 | 19, 99 | syl3an3 1302 |
. . . . . . . . 9
 
        
                 |
101 | 98, 100 | sseldd 3432 |
. . . . . . . 8
 
        
                     |
102 | 101 | eldifbd 3416 |
. . . . . . 7
 
        
       |
103 | 102 | 3expa 1207 |
. . . . . 6
             
      |
104 | 103 | ralrimiva 2801 |
. . . . 5
 
          
      |
105 | | eluni2 4201 |
. . . . . . . . 9
  
  |
106 | | ffn 5726 |
. . . . . . . . . . 11
           |
107 | 9, 106 | syl 17 |
. . . . . . . . . 10
   |
108 | | eleq2 2517 |
. . . . . . . . . . 11
     
       |
109 | 108 | rexrn 6022 |
. . . . . . . . . 10
  
        |
110 | 107, 109 | syl 17 |
. . . . . . . . 9
  

       |
111 | 105, 110 | syl5bb 261 |
. . . . . . . 8
   
       |
112 | 111 | notbid 296 |
. . . . . . 7
  
        |
113 | | ralnex 2833 |
. . . . . . 7
 
   
       |
114 | 112, 113 | syl6bbr 267 |
. . . . . 6
  
        |
115 | 114 | biimpar 488 |
. . . . 5
 
     
   |
116 | 104, 115 | syldan 473 |
. . . 4
 
         
   |
117 | 74, 116 | eldifd 3414 |
. . 3
 
                       |
118 | | ne0i 3736 |
. . 3
                         |
119 | 117, 118 | syl 17 |
. 2
 
                       |
120 | 66, 119 | exlimddv 1780 |
1
              |