Step | Hyp | Ref
| Expression |
1 | | imasval.u |
. 2
  s    |
2 | | df-imas 15418 |
. . . 4
s
        ![]_ ]_](_urbrack.gif)                                
                                    
                  Scalar   Scalar               Scalar                                              
               TopSet  
     qTop                            
inf 
                                   
                                     g                 |
3 | 2 | a1i 11 |
. . 3
 s         ![]_ ]_](_urbrack.gif)                                
                                    
                  Scalar   Scalar               Scalar                                              
               TopSet  
     qTop                            
inf 
                                   
                                     g                  |
4 | | fvex 5858 |
. . . . 5
     |
5 | 4 | a1i 11 |
. . . 4
 

        |
6 | | simplrl 775 |
. . . . . . . . . 10
   
 
    
  |
7 | 6 | rneqd 5040 |
. . . . . . . . 9
   
 
    
  |
8 | | imasval.f |
. . . . . . . . . . 11
       |
9 | | forn 5779 |
. . . . . . . . . . 11
       |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
   |
11 | 10 | ad2antrr 737 |
. . . . . . . . 9
   
 
    
  |
12 | 7, 11 | eqtrd 2486 |
. . . . . . . 8
   
 
    
  |
13 | 12 | opeq2d 4143 |
. . . . . . 7
   
 
    
                |
14 | | simplrr 776 |
. . . . . . . . . . . 12
   
 
    
  |
15 | 14 | fveq2d 5852 |
. . . . . . . . . . 11
   
 
    
          |
16 | | simpr 467 |
. . . . . . . . . . 11
   
 
    
      |
17 | | imasval.v |
. . . . . . . . . . . 12
       |
18 | 17 | ad2antrr 737 |
. . . . . . . . . . 11
   
 
    
      |
19 | 15, 16, 18 | 3eqtr4d 2496 |
. . . . . . . . . 10
   
 
    
  |
20 | 6 | fveq1d 5850 |
. . . . . . . . . . . . . 14
   
 
    
          |
21 | 6 | fveq1d 5850 |
. . . . . . . . . . . . . 14
   
 
    
          |
22 | 20, 21 | opeq12d 4144 |
. . . . . . . . . . . . 13
   
 
    
                        |
23 | 14 | fveq2d 5852 |
. . . . . . . . . . . . . . . 16
   
 
    
        |
24 | | imasval.p |
. . . . . . . . . . . . . . . 16
    |
25 | 23, 24 | syl6eqr 2504 |
. . . . . . . . . . . . . . 15
   
 
    
    |
26 | 25 | oveqd 6293 |
. . . . . . . . . . . . . 14
   
 
    
  
        |
27 | 6, 26 | fveq12d 5854 |
. . . . . . . . . . . . 13
   
 
    
                   |
28 | 22, 27 | opeq12d 4144 |
. . . . . . . . . . . 12
   
 
    
                        
                      |
29 | 28 | sneqd 3948 |
. . . . . . . . . . 11
   
 
    
                                            
      |
30 | 19, 29 | iuneq12d 4274 |
. . . . . . . . . 10
   
 
    
                            
                        |
31 | 19, 30 | iuneq12d 4274 |
. . . . . . . . 9
   
 
    
                             
                         |
32 | | imasval.a |
. . . . . . . . . 10
 
                         |
33 | 32 | ad2antrr 737 |
. . . . . . . . 9
   
 
    


                        |
34 | 31, 33 | eqtr4d 2489 |
. . . . . . . 8
   
 
    
                              |
35 | 34 | opeq2d 4143 |
. . . . . . 7
   
 
    
     

             
                     |
36 | 14 | fveq2d 5852 |
. . . . . . . . . . . . . . . 16
   
 
    
          |
37 | | imasval.m |
. . . . . . . . . . . . . . . 16
     |
38 | 36, 37 | syl6eqr 2504 |
. . . . . . . . . . . . . . 15
   
 
    
     |
39 | 38 | oveqd 6293 |
. . . . . . . . . . . . . 14
   
 
    
            |
40 | 6, 39 | fveq12d 5854 |
. . . . . . . . . . . . 13
   
 
    
                    |
41 | 22, 40 | opeq12d 4144 |
. . . . . . . . . . . 12
   
 
    
                         
                      |
42 | 41 | sneqd 3948 |
. . . . . . . . . . 11
   
 
    
                                             
      |
43 | 19, 42 | iuneq12d 4274 |
. . . . . . . . . 10
   
 
    
                             
                        |
44 | 19, 43 | iuneq12d 4274 |
. . . . . . . . 9
   
 
    
                              
                         |
45 | | imasval.t |
. . . . . . . . . 10
 
                         |
46 | 45 | ad2antrr 737 |
. . . . . . . . 9
   
 
    


                        |
47 | 44, 46 | eqtr4d 2489 |
. . . . . . . 8
   
 
    
                               |
48 | 47 | opeq2d 4143 |
. . . . . . 7
   
 
    
      

             
                    
  |
49 | 13, 35, 48 | tpeq123d 4035 |
. . . . . 6
   
 
    
                             
                                    
                                        |
50 | 14 | fveq2d 5852 |
. . . . . . . . 9
   
 
    
Scalar  Scalar    |
51 | | imasval.g |
. . . . . . . . 9
Scalar   |
52 | 50, 51 | syl6eqr 2504 |
. . . . . . . 8
   
 
    
Scalar    |
53 | 52 | opeq2d 4143 |
. . . . . . 7
   
 
    
 Scalar   Scalar    Scalar      |
54 | 52 | fveq2d 5852 |
. . . . . . . . . . . 12
   
 
    
   Scalar         |
55 | | imasval.k |
. . . . . . . . . . . 12
     |
56 | 54, 55 | syl6eqr 2504 |
. . . . . . . . . . 11
   
 
    
   Scalar     |
57 | 21 | sneqd 3948 |
. . . . . . . . . . 11
   
 
    
     
        |
58 | 14 | fveq2d 5852 |
. . . . . . . . . . . . . 14
   
 
    
          |
59 | | imasval.q |
. . . . . . . . . . . . . 14
     |
60 | 58, 59 | syl6eqr 2504 |
. . . . . . . . . . . . 13
   
 
    
     |
61 | 60 | oveqd 6293 |
. . . . . . . . . . . 12
   
 
    
            |
62 | 6, 61 | fveq12d 5854 |
. . . . . . . . . . 11
   
 
    
                    |
63 | 56, 57, 62 | mpt2eq123dv 6341 |
. . . . . . . . . 10
   
 
    
    Scalar                        
         
     |
64 | 63 | iuneq2d 4275 |
. . . . . . . . 9
   
 
    
     Scalar                        

         
     |
65 | 19 | iuneq1d 4273 |
. . . . . . . . 9
   
 
    
     Scalar                        
   Scalar                         |
66 | | imasval.s |
. . . . . . . . . 10

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

 
         
     |
68 | 64, 65, 67 | 3eqtr4d 2496 |
. . . . . . . 8
   
 
    
     Scalar                        |
69 | 68 | opeq2d 4143 |
. . . . . . 7
   
 
    
      
    Scalar                       
        |
70 | 14 | fveq2d 5852 |
. . . . . . . . . . . . . . 15
   
 
    
          |
71 | | imasval.i |
. . . . . . . . . . . . . . 15
     |
72 | 70, 71 | syl6eqr 2504 |
. . . . . . . . . . . . . 14
   
 
    
     |
73 | 72 | oveqd 6293 |
. . . . . . . . . . . . 13
   
 
    
            |
74 | 22, 73 | opeq12d 4144 |
. . . . . . . . . . . 12
   
 
    
                     
                  |
75 | 74 | sneqd 3948 |
. . . . . . . . . . 11
   
 
    
                                            |
76 | 19, 75 | iuneq12d 4274 |
. . . . . . . . . 10
   
 
    
                         
                    |
77 | 19, 76 | iuneq12d 4274 |
. . . . . . . . 9
   
 
    
                          
                     |
78 | | imasval.w |
. . . . . . . . . 10
 
                     |
79 | 78 | ad2antrr 737 |
. . . . . . . . 9
   
 
    
 
             
      |
80 | 77, 79 | eqtr4d 2489 |
. . . . . . . 8
   
 
    
                            |
81 | 80 | opeq2d 4143 |
. . . . . . 7
   
 
    
      

             
                    |
82 | 53, 69, 81 | tpeq123d 4035 |
. . . . . 6
   
 
    
  Scalar   Scalar               Scalar                                              
              Scalar                      |
83 | 49, 82 | uneq12d 3557 |
. . . . 5
   
 
    
       
      
                                                    
                  Scalar   Scalar               Scalar                                              
                                      Scalar                       |
84 | 14 | fveq2d 5852 |
. . . . . . . . . 10
   
 
    
          |
85 | | imasval.j |
. . . . . . . . . 10
     |
86 | 84, 85 | syl6eqr 2504 |
. . . . . . . . 9
   
 
    
      |
87 | 86, 6 | oveq12d 6294 |
. . . . . . . 8
   
 
    
     qTop   qTop    |
88 | | imasval.o |
. . . . . . . . 9
  qTop    |
89 | 88 | ad2antrr 737 |
. . . . . . . 8
   
 
    

qTop    |
90 | 87, 89 | eqtr4d 2489 |
. . . . . . 7
   
 
    
     qTop    |
91 | 90 | opeq2d 4143 |
. . . . . 6
   
 
    
 TopSet        qTop    TopSet      |
92 | 14 | fveq2d 5852 |
. . . . . . . . . . 11
   
 
    
          |
93 | | imasval.n |
. . . . . . . . . . 11
     |
94 | 92, 93 | syl6eqr 2504 |
. . . . . . . . . 10
   
 
    
      |
95 | 6, 94 | coeq12d 4977 |
. . . . . . . . 9
   
 
    
          |
96 | 6 | cnveqd 4988 |
. . . . . . . . 9
   
 
    
    |
97 | 95, 96 | coeq12d 4977 |
. . . . . . . 8
   
 
    
                |
98 | | imasval.l |
. . . . . . . . 9
        |
99 | 98 | ad2antrr 737 |
. . . . . . . 8
   
 
    
       |
100 | 97, 99 | eqtr4d 2489 |
. . . . . . 7
   
 
    
        
 |
101 | 100 | opeq2d 4143 |
. . . . . 6
   
 
    
               
        |
102 | 19 | sqxpeqd 4838 |
. . . . . . . . . . . . . . 15
   
 
    
      |
103 | 102 | oveq1d 6291 |
. . . . . . . . . . . . . 14
   
 
    
                  |
104 | 6 | fveq1d 5850 |
. . . . . . . . . . . . . . . 16
   
 
    
                          |
105 | 104 | eqeq1d 2454 |
. . . . . . . . . . . . . . 15
   
 
    
                            |
106 | 6 | fveq1d 5850 |
. . . . . . . . . . . . . . . 16
   
 
    
                          |
107 | 106 | eqeq1d 2454 |
. . . . . . . . . . . . . . 15
   
 
    
                            |
108 | 6 | fveq1d 5850 |
. . . . . . . . . . . . . . . . 17
   
 
    
                          |
109 | 6 | fveq1d 5850 |
. . . . . . . . . . . . . . . . 17
   
 
    
                              |
110 | 108, 109 | eqeq12d 2467 |
. . . . . . . . . . . . . . . 16
   
 
    
                                                        |
111 | 110 | ralbidv 2810 |
. . . . . . . . . . . . . . 15
   
 
    
 
                                 
                                    |
112 | 105, 107,
111 | 3anbi123d 1343 |
. . . . . . . . . . . . . 14
   
 
    
                                                            
                                                               |
113 | 103, 112 | rabeqbidv 3008 |
. . . . . . . . . . . . 13
   
 
    
                                                                                                                                              |
114 | 14 | fveq2d 5852 |
. . . . . . . . . . . . . . . 16
   
 
    
          |
115 | | imasval.e |
. . . . . . . . . . . . . . . 16
     |
116 | 114, 115 | syl6eqr 2504 |
. . . . . . . . . . . . . . 15
   
 
    
      |
117 | 116 | coeq1d 4974 |
. . . . . . . . . . . . . 14
   
 
    
          |
118 | 117 | oveq2d 6292 |
. . . . . . . . . . . . 13
   
 
    
  g          g      |
119 | 113, 118 | mpteq12dv 4453 |
. . . . . . . . . . . 12
   
 
    
    
                                                                    g                                                                                  g       |
120 | 119 | rneqd 5040 |
. . . . . . . . . . 11
   
 
    
                                                                         g                                                                                  g       |
121 | 120 | iuneq2d 4275 |
. . . . . . . . . 10
   
 
    
                                                                          g         
                                                                         g       |
122 | 121 | infeq1d 7980 |
. . . . . . . . 9
   
 
    
inf                                                                           g           inf 
                                                                         g         |
123 | 12, 12, 122 | mpt2eq123dv 6341 |
. . . . . . . 8
   
 
    
  inf                                     
                                     g             
inf                                                                           g      
   |
124 | | imasval.d |
. . . . . . . . 9
   inf 
                                                                         g          |
125 | 124 | ad2antrr 737 |
. . . . . . . 8
   
 
    


inf                                                                           g      
   |
126 | 123, 125 | eqtr4d 2489 |
. . . . . . 7
   
 
    
  inf                                     
                                     g              |
127 | 126 | opeq2d 4143 |
. . . . . 6
   
 
    
       
inf                                                                           g                  
   |
128 | 91, 101, 127 | tpeq123d 4035 |
. . . . 5
   
 
    
  TopSet        qTop                          
  inf                                     
                                     g             
  TopSet                      |
129 | 83, 128 | uneq12d 3557 |
. . . 4
   
 
    
        
      
                                                    
                  Scalar   Scalar               Scalar                                              
               TopSet  
     qTop                            
inf 
                                   
                                     g                                         Scalar                       TopSet  
       
            |
130 | 5, 129 | csbied 3358 |
. . 3
 

        ![]_ ]_](_urbrack.gif)                                
                                    
                  Scalar   Scalar               Scalar                                              
               TopSet  
     qTop                            
inf 
                                   
                                     g                                         Scalar                       TopSet  
       
            |
131 | | fof 5776 |
. . . . 5
           |
132 | 8, 131 | syl 17 |
. . . 4
       |
133 | | fvex 5858 |
. . . . 5
     |
134 | 17, 133 | syl6eqel 2538 |
. . . 4
   |
135 | | fex 6124 |
. . . 4
     
   |
136 | 132, 134,
135 | syl2anc 671 |
. . 3
   |
137 | | imasval.r |
. . . 4
   |
138 | | elex 3022 |
. . . 4
   |
139 | 137, 138 | syl 17 |
. . 3
   |
140 | | tpex 6578 |
. . . . . 6
                       |
141 | | tpex 6578 |
. . . . . 6
  Scalar                     |
142 | 140, 141 | unex 6577 |
. . . . 5
       
      
          Scalar                      |
143 | | tpex 6578 |
. . . . 5
  TopSet                     |
144 | 142, 143 | unex 6577 |
. . . 4
        
      
          Scalar                       TopSet  
       
           |
145 | 144 | a1i 11 |
. . 3
                           Scalar                       TopSet  
       
            |
146 | 3, 130, 136, 139, 145 | ovmpt2d 6412 |
. 2
  s
         
      
          Scalar                       TopSet  
       
            |
147 | 1, 146 | eqtrd 2486 |
1
         
      
          Scalar                       TopSet  
       
            |