Step | Hyp | Ref
| Expression |
1 | | simpl 459 |
. . . . . 6
 
   |
2 | 1 | neeq1d 2683 |
. . . . 5
 
     |
3 | | simpr 463 |
. . . . . 6
 
   |
4 | 3 | neeq1d 2683 |
. . . . 5
 
     |
5 | 3 | oveq2d 6306 |
. . . . . . 7
 
           |
6 | 1, 5 | eleq12d 2523 |
. . . . . 6
 
             |
7 | 1 | oveq2d 6306 |
. . . . . . 7
 
           |
8 | 3, 7 | eleq12d 2523 |
. . . . . 6
 
             |
9 | 6, 8 | orbi12d 716 |
. . . . 5
 
           
             |
10 | 2, 4, 9 | 3anbi123d 1339 |
. . . 4
 
  
          

              |
11 | | eqid 2451 |
. . . 4
     


                  


              |
12 | 10, 11 | brab2a 4884 |
. . 3
     
 
 
                                |
13 | 12 | a1i 11 |
. 2
        


             
 
 
               |
14 | | ishlg.k |
. . . . 5
hlG   |
15 | | ishlg.g |
. . . . . 6
   |
16 | | elex 3054 |
. . . . . 6
   |
17 | | fveq2 5865 |
. . . . . . . . 9
           |
18 | | ishlg.p |
. . . . . . . . 9
     |
19 | 17, 18 | syl6eqr 2503 |
. . . . . . . 8
       |
20 | 19 | eleq2d 2514 |
. . . . . . . . . . 11
     
   |
21 | 19 | eleq2d 2514 |
. . . . . . . . . . 11
     
   |
22 | 20, 21 | anbi12d 717 |
. . . . . . . . . 10
      
     
    |
23 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
 Itv  Itv    |
24 | | ishlg.i |
. . . . . . . . . . . . . . 15
Itv   |
25 | 23, 24 | syl6eqr 2503 |
. . . . . . . . . . . . . 14
 Itv    |
26 | 25 | oveqd 6307 |
. . . . . . . . . . . . 13
   Itv          |
27 | 26 | eleq2d 2514 |
. . . . . . . . . . . 12
    Itv   
       |
28 | 25 | oveqd 6307 |
. . . . . . . . . . . . 13
   Itv          |
29 | 28 | eleq2d 2514 |
. . . . . . . . . . . 12
    Itv   
       |
30 | 27, 29 | orbi12d 716 |
. . . . . . . . . . 11
     Itv      Itv    
             |
31 | 30 | 3anbi3d 1345 |
. . . . . . . . . 10
  
   Itv      Itv      
              |
32 | 22, 31 | anbi12d 717 |
. . . . . . . . 9
       
    

   Itv      Itv      
 
 
               |
33 | 32 | opabbidv 4466 |
. . . . . . . 8
          
         Itv      Itv             


               |
34 | 19, 33 | mpteq12dv 4481 |
. . . . . . 7
               
         Itv      Itv               


                |
35 | | df-hlg 24646 |
. . . . . . 7
hlG                
         Itv      Itv           |
36 | | fvex 5875 |
. . . . . . . . 9
     |
37 | 18, 36 | eqeltri 2525 |
. . . . . . . 8
 |
38 | 37 | mptex 6136 |
. . . . . . 7
      


               |
39 | 34, 35, 38 | fvmpt 5948 |
. . . . . 6
 hlG                           |
40 | 15, 16, 39 | 3syl 18 |
. . . . 5
 hlG        


                |
41 | 14, 40 | syl5eq 2497 |
. . . 4
       


                |
42 | | neeq2 2687 |
. . . . . . . 8
 
   |
43 | | neeq2 2687 |
. . . . . . . 8
 
   |
44 | | oveq1 6297 |
. . . . . . . . . 10
           |
45 | 44 | eleq2d 2514 |
. . . . . . . . 9
     
       |
46 | | oveq1 6297 |
. . . . . . . . . 10
           |
47 | 46 | eleq2d 2514 |
. . . . . . . . 9
     
       |
48 | 45, 47 | orbi12d 716 |
. . . . . . . 8
                         |
49 | 42, 43, 48 | 3anbi123d 1339 |
. . . . . . 7
  
          

              |
50 | 49 | anbi2d 710 |
. . . . . 6
                 
 
 
               |
51 | 50 | opabbidv 4466 |
. . . . 5
      


                
 
 
               |
52 | 51 | adantl 468 |
. . . 4
 
      


                
 
 
               |
53 | | ishlg.c |
. . . 4
   |
54 | 37, 37 | xpex 6595 |
. . . . . 6
   |
55 | | opabssxp 4909 |
. . . . . 6
     


            
   |
56 | 54, 55 | ssexi 4548 |
. . . . 5
     


              |
57 | 56 | a1i 11 |
. . . 4
    
 
 
               |
58 | 41, 52, 53, 57 | fvmptd 5954 |
. . 3
          


               |
59 | 58 | breqd 4413 |
. 2
              


                 |
60 | | ishlg.a |
. . . 4
   |
61 | | ishlg.b |
. . . 4
   |
62 | 60, 61 | jca 535 |
. . 3
 
   |
63 | 62 | biantrurd 511 |
. 2
  
          
 
 
               |
64 | 13, 59, 63 | 3bitr4d 289 |
1
        
              |