Step | Hyp | Ref
| Expression |
1 | | hlhilset.l |
. 2
 HLHil      |
2 | | hlhilset.k |
. . . . 5
     |
3 | | elex 3022 |
. . . . . 6
   |
4 | 3 | adantr 471 |
. . . . 5
 
   |
5 | 2, 4 | syl 17 |
. . . 4
   |
6 | | hlhilset.h |
. . . . . 6
     |
7 | | fvex 5858 |
. . . . . 6
     |
8 | 6, 7 | eqeltri 2526 |
. . . . 5
 |
9 | 8 | mptex 6122 |
. . . 4
   ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        
      
      Scalar            sSet         HGMap               
                 HDMap                 |
10 | | nfcv 2593 |
. . . . 5
   |
11 | | nfcv 2593 |
. . . . . 6
   |
12 | | nfcsb1v 3347 |
. . . . . 6
  
 ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        
      
      Scalar            sSet         HGMap               
                 HDMap                |
13 | 11, 12 | nfmpt 4463 |
. . . . 5
     ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        
      
      Scalar            sSet         HGMap               
                 HDMap                 |
14 | | fveq2 5848 |
. . . . . . 7
           |
15 | 14, 6 | syl6eqr 2504 |
. . . . . 6
       |
16 | | csbeq1a 3340 |
. . . . . 6
           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        
      
      Scalar            sSet         HGMap               
                 HDMap                 ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        
      
      Scalar            sSet         HGMap               
                 HDMap                 |
17 | 15, 16 | mpteq12dv 4453 |
. . . . 5
                ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        
      
      Scalar            sSet         HGMap               
                 HDMap                   ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        
      
      Scalar            sSet         HGMap               
                 HDMap                  |
18 | | df-hlhil 35506 |
. . . . 5
HLHil                 ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        
      
      Scalar            sSet         HGMap               
                 HDMap                  |
19 | 10, 13, 17, 18 | fvmptf 5950 |
. . . 4
  
  ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        
      
      Scalar            sSet         HGMap               
                 HDMap                 HLHil     ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        
      
      Scalar            sSet         HGMap               
                 HDMap                  |
20 | 5, 9, 19 | sylancl 673 |
. . 3
 HLHil     ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        
      
      Scalar            sSet         HGMap               
                 HDMap                  |
21 | 5 | adantr 471 |
. . . 4
 
   |
22 | | fvex 5858 |
. . . . . 6
         |
23 | 22 | a1i 11 |
. . . . 5
               |
24 | | fvex 5858 |
. . . . . . 7
     |
25 | 24 | a1i 11 |
. . . . . 6
   


        
      |
26 | | id 22 |
. . . . . . . . . 10
    
      |
27 | | id 22 |
. . . . . . . . . . . . 13
        
          |
28 | | simpr 467 |
. . . . . . . . . . . . . . . 16
       |
29 | 28 | fveq2d 5852 |
. . . . . . . . . . . . . . 15
               |
30 | | simplr 767 |
. . . . . . . . . . . . . . 15
       |
31 | 29, 30 | fveq12d 5854 |
. . . . . . . . . . . . . 14
                       |
32 | | hlhilset.u |
. . . . . . . . . . . . . 14
         |
33 | 31, 32 | syl6eqr 2504 |
. . . . . . . . . . . . 13
               |
34 | 27, 33 | sylan9eqr 2508 |
. . . . . . . . . . . 12
   


        
  |
35 | 34 | fveq2d 5852 |
. . . . . . . . . . 11
   


        
          |
36 | | hlhilset.v |
. . . . . . . . . . 11
     |
37 | 35, 36 | syl6eqr 2504 |
. . . . . . . . . 10
   


        
      |
38 | 26, 37 | sylan9eqr 2508 |
. . . . . . . . 9
               
    
  |
39 | 38 | opeq2d 4143 |
. . . . . . . 8
               
    
      
         |
40 | 34 | adantr 471 |
. . . . . . . . . . 11
               
    
  |
41 | 40 | fveq2d 5852 |
. . . . . . . . . 10
               
    
        |
42 | | hlhilset.p |
. . . . . . . . . 10
    |
43 | 41, 42 | syl6eqr 2504 |
. . . . . . . . 9
               
    
    |
44 | 43 | opeq2d 4143 |
. . . . . . . 8
               
    
        
       |
45 | 28 | fveq2d 5852 |
. . . . . . . . . . . . . 14
               |
46 | 45, 30 | fveq12d 5854 |
. . . . . . . . . . . . 13
                       |
47 | | hlhilset.e |
. . . . . . . . . . . . 13
         |
48 | 46, 47 | syl6eqr 2504 |
. . . . . . . . . . . 12
               |
49 | 28 | fveq2d 5852 |
. . . . . . . . . . . . . . 15
     HGMap  HGMap    |
50 | 49, 30 | fveq12d 5854 |
. . . . . . . . . . . . . 14
      HGMap      HGMap       |
51 | | hlhilset.g |
. . . . . . . . . . . . . 14
 HGMap      |
52 | 50, 51 | syl6eqr 2504 |
. . . . . . . . . . . . 13
      HGMap       |
53 | 52 | opeq2d 4143 |
. . . . . . . . . . . 12
           
 HGMap            
   |
54 | 48, 53 | oveq12d 6294 |
. . . . . . . . . . 11
              sSet         HGMap        sSet            |
55 | | hlhilset.r |
. . . . . . . . . . 11
 sSet       
   |
56 | 54, 55 | syl6eqr 2504 |
. . . . . . . . . 10
              sSet         HGMap         |
57 | 56 | opeq2d 4143 |
. . . . . . . . 9
      Scalar            sSet         HGMap         Scalar      |
58 | 57 | ad2antrr 737 |
. . . . . . . 8
               
    
 Scalar            sSet       
 HGMap         Scalar      |
59 | 39, 44, 58 | tpeq123d 4035 |
. . . . . . 7
               
    
                    Scalar            sSet         HGMap               
      
  Scalar       |
60 | 40 | fveq2d 5852 |
. . . . . . . . . 10
               
    
          |
61 | | hlhilset.t |
. . . . . . . . . 10
     |
62 | 60, 61 | syl6eqr 2504 |
. . . . . . . . 9
               
    
     |
63 | 62 | opeq2d 4143 |
. . . . . . . 8
               
    
          
        |
64 | 28 | fveq2d 5852 |
. . . . . . . . . . . . . . . 16
     HDMap  HDMap    |
65 | 64, 30 | fveq12d 5854 |
. . . . . . . . . . . . . . 15
      HDMap      HDMap       |
66 | | hlhilset.s |
. . . . . . . . . . . . . . 15
 HDMap      |
67 | 65, 66 | syl6eqr 2504 |
. . . . . . . . . . . . . 14
      HDMap       |
68 | 67 | ad2antrr 737 |
. . . . . . . . . . . . 13
               
    
 HDMap       |
69 | 68 | fveq1d 5850 |
. . . . . . . . . . . 12
               
    
  HDMap              |
70 | 69 | fveq1d 5850 |
. . . . . . . . . . 11
               
    
   HDMap                     |
71 | 38, 38, 70 | mpt2eq123dv 6341 |
. . . . . . . . . 10
               
    
     HDMap                         |
72 | | hlhilset.i |
. . . . . . . . . 10


          |
73 | 71, 72 | syl6eqr 2504 |
. . . . . . . . 9
               
    
     HDMap             |
74 | 73 | opeq2d 4143 |
. . . . . . . 8
               
    
           HDMap                     |
75 | 63, 74 | preq12d 4028 |
. . . . . . 7
               
    
                        HDMap             
                 |
76 | 59, 75 | uneq12d 3557 |
. . . . . 6
               
    
       
      
      Scalar            sSet         HGMap               
                 HDMap                                Scalar                       |
77 | 25, 76 | csbied 3358 |
. . . . 5
   


        
      ![]_ ]_](_urbrack.gif)                      Scalar            sSet         HGMap               
                 HDMap                                Scalar                       |
78 | 23, 77 | csbied 3358 |
. . . 4
               ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        
      
      Scalar            sSet         HGMap               
                 HDMap                                Scalar                       |
79 | 21, 78 | csbied 3358 |
. . 3
 
   ![]_ ]_](_urbrack.gif)           ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)        
      
      Scalar            sSet         HGMap               
                 HDMap                                Scalar                       |
80 | 2 | simprd 469 |
. . 3
   |
81 | | tpex 6578 |
. . . . 5
                Scalar      |
82 | | prex 4615 |
. . . . 5
                |
83 | 81, 82 | unex 6577 |
. . . 4
       
      
  Scalar                      |
84 | 83 | a1i 11 |
. . 3
                  Scalar                       |
85 | 20, 79, 80, 84 | fvmptd 5938 |
. 2
  HLHil                      Scalar                       |
86 | 1, 85 | syl5eq 2498 |
1
        
      
  Scalar                       |