Proof of Theorem ovnhoilem2
Step | Hyp | Ref
| Expression |
1 | | ovnhoilem2.m |
. . . . . . . . . 10
     
   
           
Σ^                      |
2 | 1 | eleq2i 2523 |
. . . . . . . . 9

 
         
 
       
Σ^                       |
3 | | rabid 2969 |
. . . . . . . . 9
 
          
 
       
Σ^                          
   
           
Σ^                       |
4 | 2, 3 | bitri 253 |
. . . . . . . 8

           
 
       
Σ^                       |
5 | 4 | biimpi 198 |
. . . . . . 7
  
         
 
       
Σ^                       |
6 | 5 | simprd 465 |
. . . . . 6
           
 
       
Σ^                      |
7 | 6 | adantl 468 |
. . . . 5
 
           
 
       
Σ^                      |
8 | | ovnhoilem2.l |
. . . . . . . . . 10
                                |
9 | | ovnhoilem2.x |
. . . . . . . . . . 11
   |
10 | 9 | 3ad2ant1 1030 |
. . . . . . . . . 10
 
        
 
       
Σ^                       |
11 | | ovnhoilem2.a |
. . . . . . . . . . 11
       |
12 | 11 | 3ad2ant1 1030 |
. . . . . . . . . 10
 
        
 
       
Σ^                           |
13 | | ovnhoilem2.b |
. . . . . . . . . . 11
       |
14 | 13 | 3ad2ant1 1030 |
. . . . . . . . . 10
 
        
 
       
Σ^                           |
15 | | elmapi 7498 |
. . . . . . . . . . . . . . . . . . 19
      
          |
16 | 15 | ffvelrnda 6027 |
. . . . . . . . . . . . . . . . . 18
       
       
   |
17 | | elmapi 7498 |
. . . . . . . . . . . . . . . . . 18
                     |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . 17
       
             |
19 | 18 | ffvelrnda 6027 |
. . . . . . . . . . . . . . . 16
      
 


            |
20 | | xp1st 6828 |
. . . . . . . . . . . . . . . 16
                         |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . 15
      
 


              |
22 | | eqid 2453 |
. . . . . . . . . . . . . . 15
                             |
23 | 21, 22 | fmptd 6051 |
. . . . . . . . . . . . . 14
       
                     |
24 | | reex 9635 |
. . . . . . . . . . . . . . . 16
 |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
       
   |
26 | | 1nn 10627 |
. . . . . . . . . . . . . . . . . . 19
 |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
      
  |
28 | 15, 27 | ffvelrnd 6028 |
. . . . . . . . . . . . . . . . 17
      
      
   |
29 | | elmapex 7497 |
. . . . . . . . . . . . . . . . . 18
           
   |
30 | 29 | simprd 465 |
. . . . . . . . . . . . . . . . 17
           |
31 | 28, 30 | syl 17 |
. . . . . . . . . . . . . . . 16
      
  |
32 | 31 | adantr 467 |
. . . . . . . . . . . . . . 15
       
   |
33 | | elmapg 7490 |
. . . . . . . . . . . . . . 15
 
                                       |
34 | 25, 32, 33 | syl2anc 667 |
. . . . . . . . . . . . . 14
       
                                       |
35 | 23, 34 | mpbird 236 |
. . . . . . . . . . . . 13
       
                   |
36 | | eqid 2453 |
. . . . . . . . . . . . 13
                                 |
37 | 35, 36 | fmptd 6051 |
. . . . . . . . . . . 12
      
                        |
38 | | id 22 |
. . . . . . . . . . . . . 14
      
        |
39 | | nnex 10622 |
. . . . . . . . . . . . . . . 16
 |
40 | 39 | mptex 6141 |
. . . . . . . . . . . . . . 15
                 |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . 14
      
                  |
42 | | ovnhoilem2.f |
. . . . . . . . . . . . . . 15
    
                    |
43 | 42 | fvmpt2 5962 |
. . . . . . . . . . . . . 14
       
                                       |
44 | 38, 41, 43 | syl2anc 667 |
. . . . . . . . . . . . 13
      
                      |
45 | 44 | feq1d 5719 |
. . . . . . . . . . . 12
      
          
                         |
46 | 37, 45 | mpbird 236 |
. . . . . . . . . . 11
      
            |
47 | 46 | 3ad2ant2 1031 |
. . . . . . . . . 10
 
        
 
       
Σ^                             
   |
48 | | xp2nd 6829 |
. . . . . . . . . . . . . . . 16
                         |
49 | 19, 48 | syl 17 |
. . . . . . . . . . . . . . 15
      
 


              |
50 | | eqid 2453 |
. . . . . . . . . . . . . . 15
                             |
51 | 49, 50 | fmptd 6051 |
. . . . . . . . . . . . . 14
       
                     |
52 | | elmapg 7490 |
. . . . . . . . . . . . . . 15
 
                                       |
53 | 25, 32, 52 | syl2anc 667 |
. . . . . . . . . . . . . 14
       
                                       |
54 | 51, 53 | mpbird 236 |
. . . . . . . . . . . . 13
       
                   |
55 | | eqid 2453 |
. . . . . . . . . . . . 13
                                 |
56 | 54, 55 | fmptd 6051 |
. . . . . . . . . . . 12
      
                        |
57 | 39 | mptex 6141 |
. . . . . . . . . . . . . . 15
                 |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . 14
      
                  |
59 | | ovnhoilem2.s |
. . . . . . . . . . . . . . 15
    
                    |
60 | 59 | fvmpt2 5962 |
. . . . . . . . . . . . . 14
       
                                       |
61 | 38, 58, 60 | syl2anc 667 |
. . . . . . . . . . . . 13
      
                      |
62 | 61 | feq1d 5719 |
. . . . . . . . . . . 12
      
          
                         |
63 | 56, 62 | mpbird 236 |
. . . . . . . . . . 11
      
            |
64 | 63 | 3ad2ant2 1031 |
. . . . . . . . . 10
 
        
 
       
Σ^                             
   |
65 | | simp3 1011 |
. . . . . . . . . . . 12
 
                                 |
66 | | ovnhoilem2.i |
. . . . . . . . . . . . . 14
              |
67 | 66 | a1i 11 |
. . . . . . . . . . . . 13
 
                                  |
68 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
69 | 68 | fveq1d 5872 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
70 | 69 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . 20
                           |
71 | 69 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . 20
                           |
72 | 70, 71 | oveq12d 6313 |
. . . . . . . . . . . . . . . . . . 19
                                                           |
73 | 72 | ixpeq2dv 7543 |
. . . . . . . . . . . . . . . . . 18
 
                            
                              |
74 | 73 | cbviunv 4320 |
. . . . . . . . . . . . . . . . 17
                                                             |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . 16
      
                                                              |
76 | 15 | ffvelrnda 6027 |
. . . . . . . . . . . . . . . . . . . . 21
       
       
   |
77 | | elmapi 7498 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
       
             |
79 | 78 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
      
 


        
   |
80 | | simpr 463 |
. . . . . . . . . . . . . . . . . . 19
      
 


  |
81 | 79, 80 | fvovco 37479 |
. . . . . . . . . . . . . . . . . 18
      
 


                                        |
82 | 81 | ixpeq2dva 7542 |
. . . . . . . . . . . . . . . . 17
       
 
          
                              |
83 | 82 | iuneq2dv 4303 |
. . . . . . . . . . . . . . . 16
      
                                            |
84 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
         |
85 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
                   |
86 | 84, 85, 43 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
                       |
87 | 86 | fveq1d 5872 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
                               |
88 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
   |
89 | | mptexg 6140 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 |
90 | 31, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
                |
91 | 90 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
                 |
92 | 36 | fvmpt2 5962 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                     |
93 | 88, 91, 92 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
                                     |
94 | 87, 93 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . . . . . 22
       
                         |
95 | 94 | fveq1d 5872 |
. . . . . . . . . . . . . . . . . . . . 21
       
                                 |
96 | 95 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
      
 


                                |
97 | | eqidd 2454 |
. . . . . . . . . . . . . . . . . . . . . 22
       
                               |
98 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
 


  |
99 | 98 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
 


                  |
100 | 99 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . . 22
      
 


                          |
101 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . 22
       
   |
102 | | fvex 5880 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
       
               |
104 | 97, 100, 101, 103 | fvmptd 5959 |
. . . . . . . . . . . . . . . . . . . . 21
       
                                 |
105 | 104 | adantlr 722 |
. . . . . . . . . . . . . . . . . . . 20
      
 


                                |
106 | 96, 105 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . . 19
      
 


                          |
107 | 61 | fveq1d 5872 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
                              |
108 | 107 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
                               |
109 | | mptexg 6140 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 |
110 | 31, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
                |
111 | 110 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
                 |
112 | 55 | fvmpt2 5962 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                     |
113 | 88, 111, 112 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
                                     |
114 | 108, 113 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . . . . . 22
       
                         |
115 | 114 | fveq1d 5872 |
. . . . . . . . . . . . . . . . . . . . 21
       
                                 |
116 | 115 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
      
 


                                |
117 | | eqidd 2454 |
. . . . . . . . . . . . . . . . . . . . . 22
       
                               |
118 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
119 | 118 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . . . 23
                           |
120 | 119 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
      
 


                          |
121 | | fvex 5880 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
       
               |
123 | 117, 120,
101, 122 | fvmptd 5959 |
. . . . . . . . . . . . . . . . . . . . 21
       
                                 |
124 | 123 | adantlr 722 |
. . . . . . . . . . . . . . . . . . . 20
      
 


                                |
125 | 116, 124 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . . 19
      
 


                          |
126 | 106, 125 | oveq12d 6313 |
. . . . . . . . . . . . . . . . . 18
      
 


                                                          |
127 | 126 | ixpeq2dva 7542 |
. . . . . . . . . . . . . . . . 17
       
 
                            
                              |
128 | 127 | iuneq2dv 4303 |
. . . . . . . . . . . . . . . 16
      
                                                              |
129 | 75, 83, 128 | 3eqtr4d 2497 |
. . . . . . . . . . . . . . 15
      
                                            |
130 | 129 | adantl 468 |
. . . . . . . . . . . . . 14
 
                                                   |
131 | 130 | 3adant3 1029 |
. . . . . . . . . . . . 13
 
                                                               |
132 | 67, 131 | sseq12d 3463 |
. . . . . . . . . . . 12
 
                   
                        
                                 |
133 | 65, 132 | mpbid 214 |
. . . . . . . . . . 11
 
                   
                                            |
134 | 133 | 3adant3r 1266 |
. . . . . . . . . 10
 
        
 
       
Σ^                                 
                                |
135 | 8, 10, 12, 14, 47, 64, 134 | hoidmvle 38432 |
. . . . . . . . 9
 
        
 
       
Σ^                             Σ^                              |
136 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
137 | 136 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
           |
138 | 137 | fveq1d 5872 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
                   |
139 | 138 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                           |
140 | 139 | mpteq2dva 4492 |
. . . . . . . . . . . . . . . . . . . . . 22
                               |
141 | 140 | fveq1d 5872 |
. . . . . . . . . . . . . . . . . . . . 21
                                       |
142 | 141 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
                                       |
143 | | eqidd 2454 |
. . . . . . . . . . . . . . . . . . . . . 22
                               |
144 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
145 | 144 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . . . 23
                           |
146 | 145 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                           |
147 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
148 | | fvex 5880 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
150 | 143, 146,
147, 149 | fvmptd 5959 |
. . . . . . . . . . . . . . . . . . . . 21
                                 |
151 | 150 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 
                                 |
152 | 142, 151 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . . 19
 
                                 |
153 | 138 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                           |
154 | 153 | mpteq2dva 4492 |
. . . . . . . . . . . . . . . . . . . . . 22
                               |
155 | 154 | fveq1d 5872 |
. . . . . . . . . . . . . . . . . . . . 21
                                       |
156 | 155 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
                                       |
157 | | eqidd 2454 |
. . . . . . . . . . . . . . . . . . . . . 22
                               |
158 | 144 | fveq2d 5874 |
. . . . . . . . . . . . . . . . . . . . . . 23
                           |
159 | 158 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                           |
160 | | fvex 5880 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
161 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
162 | 157, 159,
147, 161 | fvmptd 5959 |
. . . . . . . . . . . . . . . . . . . . 21
                                 |
163 | 162 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 
                                 |
164 | 156, 163 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . . 19
 
                                 |
165 | 152, 164 | oveq12d 6313 |
. . . . . . . . . . . . . . . . . 18
 
                                                                       |
166 | 165 | fveq2d 5874 |
. . . . . . . . . . . . . . . . 17
 
                                                                               |
167 | 166 | prodeq2dv 13989 |
. . . . . . . . . . . . . . . 16
                                              
                                  |
168 | 167 | cbvmptv 4498 |
. . . . . . . . . . . . . . 15
 
                                                                                 |
169 | 168 | a1i 11 |
. . . . . . . . . . . . . 14
      
 
                                                                                  |
170 | 81 | eqcomd 2459 |
. . . . . . . . . . . . . . . . 17
      
 


                                        |
171 | 170 | fveq2d 5874 |
. . . . . . . . . . . . . . . 16
      
 


                                    
           |
172 | 171 | prodeq2dv 13989 |
. . . . . . . . . . . . . . 15
       
                                                   |
173 | 172 | mpteq2dva 4492 |
. . . . . . . . . . . . . 14
      
 
                                  
                 |
174 | 169, 173 | eqtrd 2487 |
. . . . . . . . . . . . 13
      
 
                                                                |
175 | 174 | fveq2d 5874 |
. . . . . . . . . . . 12
      
Σ^                                                 Σ^                     |
176 | 175 | 3ad2ant2 1031 |
. . . . . . . . . . 11
 
      Σ^                    Σ^                                                 Σ^                     |
177 | 94 | adantll 721 |
. . . . . . . . . . . . . . . 16
                                   |
178 | 114 | adantll 721 |
. . . . . . . . . . . . . . . 16
                                   |
179 | 177, 178 | oveq12d 6313 |
. . . . . . . . . . . . . . 15
                                                                         |
180 | 9 | ad2antrr 733 |
. . . . . . . . . . . . . . . 16
             |
181 | | ovnhoilem2.n |
. . . . . . . . . . . . . . . . 17
   |
182 | 181 | ad2antrr 733 |
. . . . . . . . . . . . . . . 16
             |
183 | 19 | adantlll 725 |
. . . . . . . . . . . . . . . . . 18
   
                     |
184 | 183, 20 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
                       |
185 | 184, 22 | fmptd 6051 |
. . . . . . . . . . . . . . . 16
                               |
186 | 183, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
                       |
187 | 186, 50 | fmptd 6051 |
. . . . . . . . . . . . . . . 16
                               |
188 | 8, 180, 182, 185, 187 | hoidmvn0val 38416 |
. . . . . . . . . . . . . . 15
                                                                                              |
189 | 179, 188 | eqtrd 2487 |
. . . . . . . . . . . . . 14
                                                                                  |
190 | 189 | mpteq2dva 4492 |
. . . . . . . . . . . . 13
 
                                  
                                               |
191 | 190 | fveq2d 5874 |
. . . . . . . . . . . 12
 
       Σ^                            Σ^                                                   |
192 | 191 | 3adant3 1029 |
. . . . . . . . . . 11
 
      Σ^                    Σ^                            Σ^                                                   |
193 | | simp3 1011 |
. . . . . . . . . . 11
 
      Σ^                    Σ^                     |
194 | 176, 192,
193 | 3eqtr4d 2497 |
. . . . . . . . . 10
 
      Σ^                    Σ^                              |
195 | 194 | 3adant3l 1265 |
. . . . . . . . 9
 
        
 
       
Σ^                     Σ^                              |
196 | 135, 195 | breqtrd 4430 |
. . . . . . . 8
 
        
 
       
Σ^                               |
197 | 196 | 3exp 1208 |
. . . . . . 7
     
     
 
       
Σ^                           
    |
198 | 197 | adantr 467 |
. . . . . 6
 
       
 
           
Σ^                           
    |
199 | 198 | rexlimdv 2879 |
. . . . 5
 
  
   
   
           
Σ^                           
   |
200 | 7, 199 | mpd 15 |
. . . 4
 
           |
201 | 200 | ralrimiva 2804 |
. . 3
            |
202 | | ssrab2 3516 |
. . . . . 6


         
 
       
Σ^                      |
203 | 1, 202 | eqsstri 3464 |
. . . . 5
 |
204 | 203 | a1i 11 |
. . . 4

  |
205 | | icossxr 11726 |
. . . . 5
    |
206 | 8, 9, 11, 13 | hoidmvcl 38414 |
. . . . 5
              |
207 | 205, 206 | sseldi 3432 |
. . . 4
           |
208 | | infxrgelb 11628 |
. . . 4
 
                 
inf               |
209 | 204, 207,
208 | syl2anc 667 |
. . 3
          inf               |
210 | 201, 209 | mpbird 236 |
. 2
        
inf     |
211 | 66 | a1i 11 |
. . . . 5
 
              |
212 | | nfv 1763 |
. . . . . 6
   |
213 | 11 | ffvelrnda 6027 |
. . . . . 6
 
       |
214 | 13 | ffvelrnda 6027 |
. . . . . . 7
 
       |
215 | 214 | rexrd 9695 |
. . . . . 6
 
       |
216 | 212, 213,
215 | hoissrrn2 38410 |
. . . . 5
             
    |
217 | 211, 216 | eqsstrd 3468 |
. . . 4

    |
218 | 9, 181, 217, 1 | ovnn0val 38383 |
. . 3
  voln*     inf     |
219 | 218 | eqcomd 2459 |
. 2
 inf    voln*       |
220 | 210, 219 | breqtrd 4430 |
1
        
 voln*       |