Step | Hyp | Ref
| Expression |
1 | | imasvalOLD.u |
. 2
  s    |
2 | | df-imasOLD 15463 |
. . . 4
s
        ![]_ ]_](_urbrack.gif)                                
                                    
                  Scalar   Scalar               Scalar                                              
               TopSet  
     qTop                            
  
                                   
                                     g                 |
3 | 2 | a1i 11 |
. . 3
 s         ![]_ ]_](_urbrack.gif)                                
                                    
                  Scalar   Scalar               Scalar                                              
               TopSet  
     qTop                            
  
                                   
                                     g                  |
4 | | fvex 5902 |
. . . . 5
     |
5 | 4 | a1i 11 |
. . . 4
 

        |
6 | | simplrl 775 |
. . . . . . . . . 10
   
 
    
  |
7 | 6 | rneqd 5084 |
. . . . . . . . 9
   
 
    
  |
8 | | imasvalOLD.f |
. . . . . . . . . . 11
       |
9 | | forn 5823 |
. . . . . . . . . . 11
       |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
   |
11 | 10 | ad2antrr 737 |
. . . . . . . . 9
   
 
    
  |
12 | 7, 11 | eqtrd 2496 |
. . . . . . . 8
   
 
    
  |
13 | 12 | opeq2d 4187 |
. . . . . . 7
   
 
    
                |
14 | | simplrr 776 |
. . . . . . . . . . . 12
   
 
    
  |
15 | 14 | fveq2d 5896 |
. . . . . . . . . . 11
   
 
    
          |
16 | | simpr 467 |
. . . . . . . . . . 11
   
 
    
      |
17 | | imasvalOLD.v |
. . . . . . . . . . . 12
       |
18 | 17 | ad2antrr 737 |
. . . . . . . . . . 11
   
 
    
      |
19 | 15, 16, 18 | 3eqtr4d 2506 |
. . . . . . . . . 10
   
 
    
  |
20 | 6 | fveq1d 5894 |
. . . . . . . . . . . . . 14
   
 
    
          |
21 | 6 | fveq1d 5894 |
. . . . . . . . . . . . . 14
   
 
    
          |
22 | 20, 21 | opeq12d 4188 |
. . . . . . . . . . . . 13
   
 
    
                        |
23 | 14 | fveq2d 5896 |
. . . . . . . . . . . . . . . 16
   
 
    
        |
24 | | imasvalOLD.p |
. . . . . . . . . . . . . . . 16
    |
25 | 23, 24 | syl6eqr 2514 |
. . . . . . . . . . . . . . 15
   
 
    
    |
26 | 25 | oveqd 6337 |
. . . . . . . . . . . . . 14
   
 
    
  
        |
27 | 6, 26 | fveq12d 5898 |
. . . . . . . . . . . . 13
   
 
    
                   |
28 | 22, 27 | opeq12d 4188 |
. . . . . . . . . . . 12
   
 
    
                        
                      |
29 | 28 | sneqd 3992 |
. . . . . . . . . . 11
   
 
    
                                            
      |
30 | 19, 29 | iuneq12d 4318 |
. . . . . . . . . 10
   
 
    
                            
                        |
31 | 19, 30 | iuneq12d 4318 |
. . . . . . . . 9
   
 
    
                             
                         |
32 | | imasvalOLD.a |
. . . . . . . . . 10
 
                         |
33 | 32 | ad2antrr 737 |
. . . . . . . . 9
   
 
    


                        |
34 | 31, 33 | eqtr4d 2499 |
. . . . . . . 8
   
 
    
                              |
35 | 34 | opeq2d 4187 |
. . . . . . 7
   
 
    
     

             
                     |
36 | 14 | fveq2d 5896 |
. . . . . . . . . . . . . . . 16
   
 
    
          |
37 | | imasvalOLD.m |
. . . . . . . . . . . . . . . 16
     |
38 | 36, 37 | syl6eqr 2514 |
. . . . . . . . . . . . . . 15
   
 
    
     |
39 | 38 | oveqd 6337 |
. . . . . . . . . . . . . 14
   
 
    
            |
40 | 6, 39 | fveq12d 5898 |
. . . . . . . . . . . . 13
   
 
    
                    |
41 | 22, 40 | opeq12d 4188 |
. . . . . . . . . . . 12
   
 
    
                         
                      |
42 | 41 | sneqd 3992 |
. . . . . . . . . . 11
   
 
    
                                             
      |
43 | 19, 42 | iuneq12d 4318 |
. . . . . . . . . 10
   
 
    
                             
                        |
44 | 19, 43 | iuneq12d 4318 |
. . . . . . . . 9
   
 
    
                              
                         |
45 | | imasvalOLD.t |
. . . . . . . . . 10
 
                         |
46 | 45 | ad2antrr 737 |
. . . . . . . . 9
   
 
    


                        |
47 | 44, 46 | eqtr4d 2499 |
. . . . . . . 8
   
 
    
                               |
48 | 47 | opeq2d 4187 |
. . . . . . 7
   
 
    
      

             
                    
  |
49 | 13, 35, 48 | tpeq123d 4079 |
. . . . . 6
   
 
    
                             
                                    
                                        |
50 | 14 | fveq2d 5896 |
. . . . . . . . 9
   
 
    
Scalar  Scalar    |
51 | | imasvalOLD.g |
. . . . . . . . 9
Scalar   |
52 | 50, 51 | syl6eqr 2514 |
. . . . . . . 8
   
 
    
Scalar    |
53 | 52 | opeq2d 4187 |
. . . . . . 7
   
 
    
 Scalar   Scalar    Scalar      |
54 | 52 | fveq2d 5896 |
. . . . . . . . . . . 12
   
 
    
   Scalar         |
55 | | imasvalOLD.k |
. . . . . . . . . . . 12
     |
56 | 54, 55 | syl6eqr 2514 |
. . . . . . . . . . 11
   
 
    
   Scalar     |
57 | 21 | sneqd 3992 |
. . . . . . . . . . 11
   
 
    
     
        |
58 | 14 | fveq2d 5896 |
. . . . . . . . . . . . . 14
   
 
    
          |
59 | | imasvalOLD.q |
. . . . . . . . . . . . . 14
     |
60 | 58, 59 | syl6eqr 2514 |
. . . . . . . . . . . . 13
   
 
    
     |
61 | 60 | oveqd 6337 |
. . . . . . . . . . . 12
   
 
    
            |
62 | 6, 61 | fveq12d 5898 |
. . . . . . . . . . 11
   
 
    
                    |
63 | 56, 57, 62 | mpt2eq123dv 6385 |
. . . . . . . . . 10
   
 
    
    Scalar                        
         
     |
64 | 63 | iuneq2d 4319 |
. . . . . . . . 9
   
 
    
     Scalar                        

         
     |
65 | 19 | iuneq1d 4317 |
. . . . . . . . 9
   
 
    
     Scalar                        
   Scalar                         |
66 | | imasvalOLD.s |
. . . . . . . . . 10

                  |
67 | 66 | ad2antrr 737 |
. . . . . . . . 9
   
 
    

 
         
     |
68 | 64, 65, 67 | 3eqtr4d 2506 |
. . . . . . . 8
   
 
    
     Scalar                        |
69 | 68 | opeq2d 4187 |
. . . . . . 7
   
 
    
      
    Scalar                       
        |
70 | 14 | fveq2d 5896 |
. . . . . . . . . . . . . . 15
   
 
    
          |
71 | | imasvalOLD.i |
. . . . . . . . . . . . . . 15
     |
72 | 70, 71 | syl6eqr 2514 |
. . . . . . . . . . . . . 14
   
 
    
     |
73 | 72 | oveqd 6337 |
. . . . . . . . . . . . 13
   
 
    
            |
74 | 22, 73 | opeq12d 4188 |
. . . . . . . . . . . 12
   
 
    
                     
                  |
75 | 74 | sneqd 3992 |
. . . . . . . . . . 11
   
 
    
                                            |
76 | 19, 75 | iuneq12d 4318 |
. . . . . . . . . 10
   
 
    
                         
                    |
77 | 19, 76 | iuneq12d 4318 |
. . . . . . . . 9
   
 
    
                          
                     |
78 | | imasvalOLD.w |
. . . . . . . . . 10
 
                     |
79 | 78 | ad2antrr 737 |
. . . . . . . . 9
   
 
    
 
             
      |
80 | 77, 79 | eqtr4d 2499 |
. . . . . . . 8
   
 
    
                            |
81 | 80 | opeq2d 4187 |
. . . . . . 7
   
 
    
      

             
                    |
82 | 53, 69, 81 | tpeq123d 4079 |
. . . . . 6
   
 
    
  Scalar   Scalar               Scalar                                              
              Scalar                      |
83 | 49, 82 | uneq12d 3601 |
. . . . 5
   
 
    
       
      
                                                    
                  Scalar   Scalar               Scalar                                              
                                      Scalar                       |
84 | 14 | fveq2d 5896 |
. . . . . . . . . 10
   
 
    
          |
85 | | imasvalOLD.j |
. . . . . . . . . 10
     |
86 | 84, 85 | syl6eqr 2514 |
. . . . . . . . 9
   
 
    
      |
87 | 86, 6 | oveq12d 6338 |
. . . . . . . 8
   
 
    
     qTop   qTop    |
88 | | imasvalOLD.o |
. . . . . . . . 9
  qTop    |
89 | 88 | ad2antrr 737 |
. . . . . . . 8
   
 
    

qTop    |
90 | 87, 89 | eqtr4d 2499 |
. . . . . . 7
   
 
    
     qTop    |
91 | 90 | opeq2d 4187 |
. . . . . 6
   
 
    
 TopSet        qTop    TopSet      |
92 | 14 | fveq2d 5896 |
. . . . . . . . . . 11
   
 
    
          |
93 | | imasvalOLD.n |
. . . . . . . . . . 11
     |
94 | 92, 93 | syl6eqr 2514 |
. . . . . . . . . 10
   
 
    
      |
95 | 6, 94 | coeq12d 5021 |
. . . . . . . . 9
   
 
    
          |
96 | 6 | cnveqd 5032 |
. . . . . . . . 9
   
 
    
    |
97 | 95, 96 | coeq12d 5021 |
. . . . . . . 8
   
 
    
                |
98 | | imasvalOLD.l |
. . . . . . . . 9
        |
99 | 98 | ad2antrr 737 |
. . . . . . . 8
   
 
    
       |
100 | 97, 99 | eqtr4d 2499 |
. . . . . . 7
   
 
    
        
 |
101 | 100 | opeq2d 4187 |
. . . . . 6
   
 
    
               
        |
102 | 19 | sqxpeqd 4882 |
. . . . . . . . . . . . . . 15
   
 
    
      |
103 | 102 | oveq1d 6335 |
. . . . . . . . . . . . . 14
   
 
    
                  |
104 | 6 | fveq1d 5894 |
. . . . . . . . . . . . . . . 16
   
 
    
                          |
105 | 104 | eqeq1d 2464 |
. . . . . . . . . . . . . . 15
   
 
    
                            |
106 | 6 | fveq1d 5894 |
. . . . . . . . . . . . . . . 16
   
 
    
                          |
107 | 106 | eqeq1d 2464 |
. . . . . . . . . . . . . . 15
   
 
    
                            |
108 | 6 | fveq1d 5894 |
. . . . . . . . . . . . . . . . 17
   
 
    
                          |
109 | 6 | fveq1d 5894 |
. . . . . . . . . . . . . . . . 17
   
 
    
                              |
110 | 108, 109 | eqeq12d 2477 |
. . . . . . . . . . . . . . . 16
   
 
    
                                                        |
111 | 110 | ralbidv 2839 |
. . . . . . . . . . . . . . 15
   
 
    
 
                                 
                                    |
112 | 105, 107,
111 | 3anbi123d 1348 |
. . . . . . . . . . . . . 14
   
 
    
                                                            
                                                               |
113 | 103, 112 | rabeqbidv 3052 |
. . . . . . . . . . . . 13
   
 
    
                                                                                                                                              |
114 | 14 | fveq2d 5896 |
. . . . . . . . . . . . . . . 16
   
 
    
          |
115 | | imasvalOLD.e |
. . . . . . . . . . . . . . . 16
     |
116 | 114, 115 | syl6eqr 2514 |
. . . . . . . . . . . . . . 15
   
 
    
      |
117 | 116 | coeq1d 5018 |
. . . . . . . . . . . . . 14
   
 
    
          |
118 | 117 | oveq2d 6336 |
. . . . . . . . . . . . 13
   
 
    
  g          g      |
119 | 113, 118 | mpteq12dv 4497 |
. . . . . . . . . . . 12
   
 
    
    
                                                                    g                                                                                  g       |
120 | 119 | rneqd 5084 |
. . . . . . . . . . 11
   
 
    
                                                                         g                                                                                  g       |
121 | 120 | iuneq2d 4319 |
. . . . . . . . . 10
   
 
    
                                                                          g         
                                                                         g       |
122 | 121 | supeq1d 7991 |
. . . . . . . . 9
   
 
    
  
                                   
                                     g                                                                                       g         |
123 | 12, 12, 122 | mpt2eq123dv 6385 |
. . . . . . . 8
   
 
    
                                                                              g             
                                                                            g      
   |
124 | | imasvalOLD.d |
. . . . . . . . 9
     
                                                                         g          |
125 | 124 | ad2antrr 737 |
. . . . . . . 8
   
 
    


                                                                            g      
   |
126 | 123, 125 | eqtr4d 2499 |
. . . . . . 7
   
 
    
                                                                              g              |
127 | 126 | opeq2d 4187 |
. . . . . 6
   
 
    
       
                                                                            g                  
   |
128 | 91, 101, 127 | tpeq123d 4079 |
. . . . 5
   
 
    
  TopSet        qTop                          
                                                                              g             
  TopSet                      |
129 | 83, 128 | uneq12d 3601 |
. . . 4
   
 
    
        
      
                                                    
                  Scalar   Scalar               Scalar                                              
               TopSet  
     qTop                            
  
                                   
                                     g                                         Scalar                       TopSet  
       
            |
130 | 5, 129 | csbied 3402 |
. . 3
 

        ![]_ ]_](_urbrack.gif)                                
                                    
                  Scalar   Scalar               Scalar                                              
               TopSet  
     qTop                            
  
                                   
                                     g                                         Scalar                       TopSet  
       
            |
131 | | fof 5820 |
. . . . 5
           |
132 | 8, 131 | syl 17 |
. . . 4
       |
133 | | fvex 5902 |
. . . . 5
     |
134 | 17, 133 | syl6eqel 2548 |
. . . 4
   |
135 | | fex 6168 |
. . . 4
     
   |
136 | 132, 134,
135 | syl2anc 671 |
. . 3
   |
137 | | imasvalOLD.r |
. . . 4
   |
138 | | elex 3066 |
. . . 4
   |
139 | 137, 138 | syl 17 |
. . 3
   |
140 | | tpex 6622 |
. . . . . 6
                       |
141 | | tpex 6622 |
. . . . . 6
  Scalar                     |
142 | 140, 141 | unex 6621 |
. . . . 5
       
      
          Scalar                      |
143 | | tpex 6622 |
. . . . 5
  TopSet                     |
144 | 142, 143 | unex 6621 |
. . . 4
        
      
          Scalar                       TopSet  
       
           |
145 | 144 | a1i 11 |
. . 3
                           Scalar                       TopSet  
       
            |
146 | 3, 130, 136, 139, 145 | ovmpt2d 6456 |
. 2
  s
         
      
          Scalar                       TopSet  
       
            |
147 | 1, 146 | eqtrd 2496 |
1
         
      
          Scalar                       TopSet  
       
            |