Step | Hyp | Ref
| Expression |
1 | | dihjatcclem.k |
. . 3
     |
2 | | dihjatcclem.h |
. . . 4
     |
3 | | dihjatcclem.i |
. . . 4
         |
4 | 2, 3 | dihvalrel 34859 |
. . 3
 
       |
5 | 1, 4 | syl 17 |
. 2
       |
6 | 1 | adantr 467 |
. . . . . . 7
 
            |
7 | | dihjatcclem.l |
. . . . . . . . . . . 12
     |
8 | | dihjatcclem.a |
. . . . . . . . . . . 12
     |
9 | | dihjatcc.w |
. . . . . . . . . . . 12
         |
10 | 7, 8, 2, 9 | lhpocnel2 33596 |
. . . . . . . . . . 11
 
     |
11 | 1, 10 | syl 17 |
. . . . . . . . . 10
     |
12 | | dihjatcclem.p |
. . . . . . . . . 10
     |
13 | | dihjatcc.t |
. . . . . . . . . . 11
         |
14 | | dihjatcc.g |
. . . . . . . . . . 11
        |
15 | 7, 8, 2, 13, 14 | ltrniotacl 34158 |
. . . . . . . . . 10
      
 
  |
16 | 1, 11, 12, 15 | syl3anc 1269 |
. . . . . . . . 9
   |
17 | | dihjatcclem.q |
. . . . . . . . . . 11
     |
18 | | dihjatcc.dd |
. . . . . . . . . . . 12
        |
19 | 7, 8, 2, 13, 18 | ltrniotacl 34158 |
. . . . . . . . . . 11
      
 
  |
20 | 1, 11, 17, 19 | syl3anc 1269 |
. . . . . . . . . 10
   |
21 | 2, 13 | ltrncnv 33723 |
. . . . . . . . . 10
    
   |
22 | 1, 20, 21 | syl2anc 667 |
. . . . . . . . 9
 
  |
23 | 2, 13 | ltrnco 34298 |
. . . . . . . . 9
    

     |
24 | 1, 16, 22, 23 | syl3anc 1269 |
. . . . . . . 8
      |
25 | 24 | adantr 467 |
. . . . . . 7
 
             |
26 | | simprll 773 |
. . . . . . 7
 
          |
27 | | simprlr 774 |
. . . . . . . 8
 
              |
28 | | dihjatcclem.b |
. . . . . . . . . 10
     |
29 | | dihjatcclem.j |
. . . . . . . . . 10
     |
30 | | dihjatcclem.m |
. . . . . . . . . 10
     |
31 | | dihjatcclem.u |
. . . . . . . . . 10
         |
32 | | dihjatcclem.s |
. . . . . . . . . 10
     |
33 | | dihjatcclem.v |
. . . . . . . . . 10
  
  |
34 | | dihjatcc.r |
. . . . . . . . . 10
         |
35 | | dihjatcc.e |
. . . . . . . . . 10
         |
36 | 28, 7, 2, 29, 30, 8, 31, 32, 3, 33, 1, 12, 17, 9, 13, 34, 35, 14, 18 | dihjatcclem3 35000 |
. . . . . . . . 9
    
     |
37 | 36 | adantr 467 |
. . . . . . . 8
 
           
     |
38 | 27, 37 | breqtrrd 4432 |
. . . . . . 7
 
               
     |
39 | 7, 2, 13, 34, 35 | tendoex 34554 |
. . . . . . 7
                
    
   
     |
40 | 6, 25, 26, 38, 39 | syl121anc 1274 |
. . . . . 6
 
        
   
     |
41 | | df-rex 2745 |
. . . . . 6
        
      
      |
42 | 40, 41 | sylib 200 |
. . . . 5
 
                     |
43 | | eqidd 2454 |
. . . . . . . . . 10
         


                   |
44 | | simprl 765 |
. . . . . . . . . 10
         


           |
45 | 1 | ad2antrr 733 |
. . . . . . . . . . 11
         


             |
46 | 12 | ad2antrr 733 |
. . . . . . . . . . 11
         


             |
47 | | fvex 5880 |
. . . . . . . . . . . 12
     |
48 | | vex 3050 |
. . . . . . . . . . . 12
 |
49 | 7, 8, 2, 9, 13, 35, 3, 14, 47, 48 | dihopelvalcqat 34826 |
. . . . . . . . . . 11
                  
             |
50 | 45, 46, 49 | syl2anc 667 |
. . . . . . . . . 10
         


                    
             |
51 | 43, 44, 50 | mpbir2and 934 |
. . . . . . . . 9
         


                      |
52 | | eqidd 2454 |
. . . . . . . . . 10
         


                           |
53 | | dihjatcc.n |
. . . . . . . . . . . 12
          |
54 | 2, 13, 35, 53 | tendoicl 34375 |
. . . . . . . . . . 11
    
      |
55 | 45, 44, 54 | syl2anc 667 |
. . . . . . . . . 10
         


               |
56 | 17 | ad2antrr 733 |
. . . . . . . . . . 11
         


             |
57 | | fvex 5880 |
. . . . . . . . . . . 12
         |
58 | | fvex 5880 |
. . . . . . . . . . . 12
     |
59 | 7, 8, 2, 9, 13, 35, 3, 18, 57, 58 | dihopelvalcqat 34826 |
. . . . . . . . . . 11
                          
                         |
60 | 45, 56, 59 | syl2anc 667 |
. . . . . . . . . 10
         


                            
                         |
61 | 52, 55, 60 | mpbir2and 934 |
. . . . . . . . 9
         


                              |
62 | 16 | ad2antrr 733 |
. . . . . . . . . . 11
         


        
  |
63 | 22 | ad2antrr 733 |
. . . . . . . . . . 11
         


         
  |
64 | 2, 13, 35 | tendospdi1 34600 |
. . . . . . . . . . 11
           
                |
65 | 45, 44, 62, 63, 64 | syl13anc 1271 |
. . . . . . . . . 10
         


            
                |
66 | | simprr 767 |
. . . . . . . . . 10
         


            
     |
67 | 20 | ad2antrr 733 |
. . . . . . . . . . . . 13
         


        
  |
68 | 53, 13 | tendoi2 34374 |
. . . . . . . . . . . . 13
 
                |
69 | 44, 67, 68 | syl2anc 667 |
. . . . . . . . . . . 12
         


                        |
70 | 2, 13, 35 | tendocnv 34601 |
. . . . . . . . . . . . 13
   

            |
71 | 45, 44, 67, 70 | syl3anc 1269 |
. . . . . . . . . . . 12
         


                     |
72 | 69, 71 | eqtr2d 2488 |
. . . . . . . . . . 11
         


                        |
73 | 72 | coeq2d 5000 |
. . . . . . . . . 10
         


                                    |
74 | 65, 66, 73 | 3eqtr3d 2495 |
. . . . . . . . 9
         


                         |
75 | | simplrr 772 |
. . . . . . . . . 10
         


          |
76 | | dihjatcc.d |
. . . . . . . . . . . 12
 
              |
77 | | dihjatcc.o |
. . . . . . . . . . . 12
    |
78 | 2, 13, 35, 53, 28, 76, 77 | tendoipl2 34377 |
. . . . . . . . . . 11
    
         |
79 | 45, 44, 78 | syl2anc 667 |
. . . . . . . . . 10
         


                  |
80 | 75, 79 | eqtr4d 2490 |
. . . . . . . . 9
         


                   |
81 | | opeq1 4169 |
. . . . . . . . . . . . . . 15
                 |
82 | 81 | eleq1d 2515 |
. . . . . . . . . . . . . 14
                           |
83 | 82 | anbi1d 712 |
. . . . . . . . . . . . 13
                                             |
84 | | coeq1 4995 |
. . . . . . . . . . . . . . 15
               |
85 | 84 | eqeq2d 2463 |
. . . . . . . . . . . . . 14
       
         |
86 | 85 | anbi1d 712 |
. . . . . . . . . . . . 13
                    
        |
87 | 83, 86 | anbi12d 718 |
. . . . . . . . . . . 12
                               
            
  
    
                |
88 | | opeq1 4169 |
. . . . . . . . . . . . . . 15
           
             |
89 | 88 | eleq1d 2515 |
. . . . . . . . . . . . . 14
                                   |
90 | 89 | anbi2d 711 |
. . . . . . . . . . . . 13
                                                             |
91 | | coeq2 4996 |
. . . . . . . . . . . . . . 15
                               |
92 | 91 | eqeq2d 2463 |
. . . . . . . . . . . . . 14
               
                 |
93 | 92 | anbi1d 712 |
. . . . . . . . . . . . 13
                                    
        |
94 | 90, 93 | anbi12d 718 |
. . . . . . . . . . . 12
                                           
            
          
    
                        |
95 | | opeq2 4170 |
. . . . . . . . . . . . . . 15
               
                 |
96 | 95 | eleq1d 2515 |
. . . . . . . . . . . . . 14
                                           |
97 | 96 | anbi2d 711 |
. . . . . . . . . . . . 13
                            
                                        |
98 | | oveq2 6303 |
. . . . . . . . . . . . . . 15
                   |
99 | 98 | eqeq2d 2463 |
. . . . . . . . . . . . . 14
         
           |
100 | 99 | anbi2d 711 |
. . . . . . . . . . . . 13
                                        
            |
101 | 97, 100 | anbi12d 718 |
. . . . . . . . . . . 12
                                                       
            
                                  
             |
102 | 87, 94, 101 | syl3an9b 1339 |
. . . . . . . . . . 11
     
                      
  
    
                                                                      |
103 | 102 | spc3egv 3140 |
. . . . . . . . . 10
                                
                                  
                        
  
    
            |
104 | 47, 57, 58, 103 | mp3an 1366 |
. . . . . . . . 9
                                                                         
  
    
           |
105 | 51, 61, 74, 80, 104 | syl22anc 1270 |
. . . . . . . 8
         


                       
  
    
           |
106 | 105 | ex 436 |
. . . . . . 7
 
                                                     |
107 | 106 | eximdv 1766 |
. . . . . 6
 
               
   
                
  
    
            |
108 | | excom 1929 |
. . . . . 6
                                                                       |
109 | 107, 108 | syl6ib 230 |
. . . . 5
 
               
   
                
  
    
            |
110 | 42, 109 | mpd 15 |
. . . 4
 
                                            |
111 | 110 | ex 436 |
. . 3
                         
  
    
            |
112 | 1 | simpld 461 |
. . . . . . . . 9
   |
113 | | hllat 32941 |
. . . . . . . . 9
   |
114 | 112, 113 | syl 17 |
. . . . . . . 8
   |
115 | 12 | simpld 461 |
. . . . . . . . 9
   |
116 | 17 | simpld 461 |
. . . . . . . . 9
   |
117 | 28, 29, 8 | hlatjcl 32944 |
. . . . . . . . 9
 
     |
118 | 112, 115,
116, 117 | syl3anc 1269 |
. . . . . . . 8
     |
119 | 1 | simprd 465 |
. . . . . . . . 9
   |
120 | 28, 2 | lhpbase 33575 |
. . . . . . . . 9
   |
121 | 119, 120 | syl 17 |
. . . . . . . 8
   |
122 | 28, 30 | latmcl 16310 |
. . . . . . . 8
  
    
   |
123 | 114, 118,
121, 122 | syl3anc 1269 |
. . . . . . 7
   
   |
124 | 33, 123 | syl5eqel 2535 |
. . . . . 6
   |
125 | 28, 7, 30 | latmle2 16335 |
. . . . . . . 8
  
    
   |
126 | 114, 118,
121, 125 | syl3anc 1269 |
. . . . . . 7
   
   |
127 | 33, 126 | syl5eqbr 4439 |
. . . . . 6

  |
128 | | eqid 2453 |
. . . . . . 7
                 |
129 | 28, 7, 2, 3, 128 | dihvalb 34817 |
. . . . . 6
                         |
130 | 1, 124, 127, 129 | syl12anc 1267 |
. . . . 5
                   |
131 | 130 | eleq2d 2516 |
. . . 4
        
  
               |
132 | 28, 7, 2, 13, 34, 77, 128 | dibopelval3 34728 |
. . . . 5
                             
   |
133 | 1, 124, 127, 132 | syl12anc 1267 |
. . . 4
                           |
134 | 131, 133 | bitrd 257 |
. . 3
        
          |
135 | | eqid 2453 |
. . . 4
         |
136 | 28, 8 | atbase 32867 |
. . . . 5
   |
137 | 115, 136 | syl 17 |
. . . 4
   |
138 | 28, 8 | atbase 32867 |
. . . . 5
   |
139 | 116, 138 | syl 17 |
. . . 4
   |
140 | 28, 2, 13, 35, 76, 31, 135, 32, 3, 1, 137, 139 | dihopellsm 34835 |
. . 3
                                                    |
141 | 111, 134,
140 | 3imtr4d 272 |
. 2
                         |
142 | 5, 141 | relssdv 4930 |
1
    
            |