Proof of Theorem ovnhoilem2
Step | Hyp | Ref
| Expression |
1 | | ovnhoilem2.m |
. . . . . . . . . 10
Σ^ |
2 | 1 | eleq2i 2693 |
. . . . . . . . 9
Σ^ |
3 | | rabid 3116 |
. . . . . . . . 9
Σ^
Σ^ |
4 | 2, 3 | bitri 264 |
. . . . . . . 8
Σ^ |
5 | 4 | biimpi 206 |
. . . . . . 7
Σ^ |
6 | 5 | simprd 479 |
. . . . . 6
Σ^ |
7 | 6 | adantl 482 |
. . . . 5
Σ^ |
8 | | ovnhoilem2.l |
. . . . . . . . . 10
|
9 | | ovnhoilem2.x |
. . . . . . . . . . 11
|
10 | 9 | 3ad2ant1 1082 |
. . . . . . . . . 10
Σ^ |
11 | | ovnhoilem2.a |
. . . . . . . . . . 11
|
12 | 11 | 3ad2ant1 1082 |
. . . . . . . . . 10
Σ^ |
13 | | ovnhoilem2.b |
. . . . . . . . . . 11
|
14 | 13 | 3ad2ant1 1082 |
. . . . . . . . . 10
Σ^ |
15 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . 19
|
16 | 15 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . 18
|
17 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . 18
|
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
19 | 18 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
|
20 | | xp1st 7198 |
. . . . . . . . . . . . . . . 16
|
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . 15
|
22 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
23 | 21, 22 | fmptd 6385 |
. . . . . . . . . . . . . 14
|
24 | | reex 10027 |
. . . . . . . . . . . . . . . 16
|
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
|
26 | | 1nn 11031 |
. . . . . . . . . . . . . . . . . . 19
|
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
28 | 15, 27 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
|
29 | | elmapex 7878 |
. . . . . . . . . . . . . . . . . 18
|
30 | 29 | simprd 479 |
. . . . . . . . . . . . . . . . 17
|
31 | 28, 30 | syl 17 |
. . . . . . . . . . . . . . . 16
|
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . 15
|
33 | | elmapg 7870 |
. . . . . . . . . . . . . . 15
|
34 | 25, 32, 33 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
35 | 23, 34 | mpbird 247 |
. . . . . . . . . . . . 13
|
36 | | eqid 2622 |
. . . . . . . . . . . . 13
|
37 | 35, 36 | fmptd 6385 |
. . . . . . . . . . . 12
|
38 | | id 22 |
. . . . . . . . . . . . . 14
|
39 | | nnex 11026 |
. . . . . . . . . . . . . . . 16
|
40 | 39 | mptex 6486 |
. . . . . . . . . . . . . . 15
|
41 | 40 | a1i 11 |
. . . . . . . . . . . . . 14
|
42 | | ovnhoilem2.f |
. . . . . . . . . . . . . . 15
|
43 | 42 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
|
44 | 38, 41, 43 | syl2anc 693 |
. . . . . . . . . . . . 13
|
45 | 44 | feq1d 6030 |
. . . . . . . . . . . 12
|
46 | 37, 45 | mpbird 247 |
. . . . . . . . . . 11
|
47 | 46 | 3ad2ant2 1083 |
. . . . . . . . . 10
Σ^
|
48 | | xp2nd 7199 |
. . . . . . . . . . . . . . . 16
|
49 | 19, 48 | syl 17 |
. . . . . . . . . . . . . . 15
|
50 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
51 | 49, 50 | fmptd 6385 |
. . . . . . . . . . . . . 14
|
52 | | elmapg 7870 |
. . . . . . . . . . . . . . 15
|
53 | 25, 32, 52 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
54 | 51, 53 | mpbird 247 |
. . . . . . . . . . . . 13
|
55 | | eqid 2622 |
. . . . . . . . . . . . 13
|
56 | 54, 55 | fmptd 6385 |
. . . . . . . . . . . 12
|
57 | 39 | mptex 6486 |
. . . . . . . . . . . . . . 15
|
58 | 57 | a1i 11 |
. . . . . . . . . . . . . 14
|
59 | | ovnhoilem2.s |
. . . . . . . . . . . . . . 15
|
60 | 59 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
|
61 | 38, 58, 60 | syl2anc 693 |
. . . . . . . . . . . . 13
|
62 | 61 | feq1d 6030 |
. . . . . . . . . . . 12
|
63 | 56, 62 | mpbird 247 |
. . . . . . . . . . 11
|
64 | 63 | 3ad2ant2 1083 |
. . . . . . . . . 10
Σ^
|
65 | | simp3 1063 |
. . . . . . . . . . . 12
|
66 | | ovnhoilem2.i |
. . . . . . . . . . . . . 14
|
67 | 66 | a1i 11 |
. . . . . . . . . . . . 13
|
68 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
|
69 | 68 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . 21
|
70 | 69 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
71 | 69 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 70, 71 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 72 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . . . . 18
|
74 | 73 | cbviunv 4559 |
. . . . . . . . . . . . . . . . 17
|
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
76 | 15 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . 21
|
77 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . 21
|
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | 78 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
80 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
|
81 | 79, 80 | fvovco 39381 |
. . . . . . . . . . . . . . . . . 18
|
82 | 81 | ixpeq2dva 7923 |
. . . . . . . . . . . . . . . . 17
|
83 | 82 | iuneq2dv 4542 |
. . . . . . . . . . . . . . . 16
|
84 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
85 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
86 | 84, 85, 43 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
87 | 86 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
88 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
89 | | mptexg 6484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
90 | 31, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
91 | 90 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
92 | 36 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
93 | 88, 91, 92 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
94 | 87, 93 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
|
95 | 94 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . 21
|
96 | 95 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
97 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . 22
|
98 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
99 | 98 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
100 | 99 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
|
101 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
|
102 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . 22
|
103 | 97, 100, 101, 102 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . 21
|
104 | 103 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
|
105 | 96, 104 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
106 | 61 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
107 | 106 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
108 | | mptexg 6484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
109 | 31, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
110 | 109 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
111 | 55 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
112 | 88, 110, 111 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
113 | 107, 112 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
|
114 | 113 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . 21
|
115 | 114 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
116 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . 22
|
117 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
118 | 117 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
119 | 118 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
120 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . 22
|
121 | 116, 119,
101, 120 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . 21
|
122 | 121 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
|
123 | 115, 122 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
124 | 105, 123 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
|
125 | 124 | ixpeq2dva 7923 |
. . . . . . . . . . . . . . . . 17
|
126 | 125 | iuneq2dv 4542 |
. . . . . . . . . . . . . . . 16
|
127 | 75, 83, 126 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . 15
|
128 | 127 | adantl 482 |
. . . . . . . . . . . . . 14
|
129 | 128 | 3adant3 1081 |
. . . . . . . . . . . . 13
|
130 | 67, 129 | sseq12d 3634 |
. . . . . . . . . . . 12
|
131 | 65, 130 | mpbid 222 |
. . . . . . . . . . 11
|
132 | 131 | 3adant3r 1323 |
. . . . . . . . . 10
Σ^
|
133 | 8, 10, 12, 14, 47, 64, 132 | hoidmvle 40814 |
. . . . . . . . 9
Σ^ Σ^ |
134 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
135 | 134 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
136 | 135 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
137 | 136 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
138 | 137 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . . . . . 22
|
139 | 138 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . 21
|
140 | 139 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
141 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . 22
|
142 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
143 | 142 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
144 | 143 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
145 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
|
146 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . 22
|
147 | 141, 144,
145, 146 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . 21
|
148 | 147 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
149 | 140, 148 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
150 | 136 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
151 | 150 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . . . . . 22
|
152 | 151 | fveq1d 6193 |
. . . . . . . . . . . . . . . . . . . . 21
|
153 | 152 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
154 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . . . 22
|
155 | 142 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
156 | 155 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
|
157 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . 22
|
158 | 154, 156,
145, 157 | fvmptd 6288 |
. . . . . . . . . . . . . . . . . . . . 21
|
159 | 158 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
160 | 153, 159 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
161 | 149, 160 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
|
162 | 161 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
163 | 162 | prodeq2dv 14653 |
. . . . . . . . . . . . . . . 16
|
164 | 163 | cbvmptv 4750 |
. . . . . . . . . . . . . . 15
|
165 | 164 | a1i 11 |
. . . . . . . . . . . . . 14
|
166 | 81 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
|
167 | 166 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
168 | 167 | prodeq2dv 14653 |
. . . . . . . . . . . . . . 15
|
169 | 168 | mpteq2dva 4744 |
. . . . . . . . . . . . . 14
|
170 | 165, 169 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
171 | 170 | fveq2d 6195 |
. . . . . . . . . . . 12
Σ^ Σ^ |
172 | 171 | 3ad2ant2 1083 |
. . . . . . . . . . 11
Σ^ Σ^ Σ^ |
173 | 94 | adantll 750 |
. . . . . . . . . . . . . . . 16
|
174 | 113 | adantll 750 |
. . . . . . . . . . . . . . . 16
|
175 | 173, 174 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
176 | 9 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
177 | | ovnhoilem2.n |
. . . . . . . . . . . . . . . . 17
|
178 | 177 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
179 | 19 | adantlll 754 |
. . . . . . . . . . . . . . . . . 18
|
180 | 179, 20 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
181 | 180, 22 | fmptd 6385 |
. . . . . . . . . . . . . . . 16
|
182 | 179, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
183 | 182, 50 | fmptd 6385 |
. . . . . . . . . . . . . . . 16
|
184 | 8, 176, 178, 181, 183 | hoidmvn0val 40798 |
. . . . . . . . . . . . . . 15
|
185 | 175, 184 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
186 | 185 | mpteq2dva 4744 |
. . . . . . . . . . . . 13
|
187 | 186 | fveq2d 6195 |
. . . . . . . . . . . 12
Σ^ Σ^ |
188 | 187 | 3adant3 1081 |
. . . . . . . . . . 11
Σ^ Σ^ Σ^ |
189 | | simp3 1063 |
. . . . . . . . . . 11
Σ^ Σ^ |
190 | 172, 188,
189 | 3eqtr4d 2666 |
. . . . . . . . . 10
Σ^ Σ^ |
191 | 190 | 3adant3l 1322 |
. . . . . . . . 9
Σ^ Σ^ |
192 | 133, 191 | breqtrd 4679 |
. . . . . . . 8
Σ^ |
193 | 192 | 3exp 1264 |
. . . . . . 7
Σ^
|
194 | 193 | adantr 481 |
. . . . . 6
Σ^
|
195 | 194 | rexlimdv 3030 |
. . . . 5
Σ^
|
196 | 7, 195 | mpd 15 |
. . . 4
|
197 | 196 | ralrimiva 2966 |
. . 3
|
198 | | ssrab2 3687 |
. . . . . 6
Σ^ |
199 | 1, 198 | eqsstri 3635 |
. . . . 5
|
200 | 199 | a1i 11 |
. . . 4
|
201 | | icossxr 12258 |
. . . . 5
|
202 | 8, 9, 11, 13 | hoidmvcl 40796 |
. . . . 5
|
203 | 201, 202 | sseldi 3601 |
. . . 4
|
204 | | infxrgelb 12165 |
. . . 4
inf |
205 | 200, 203,
204 | syl2anc 693 |
. . 3
inf |
206 | 197, 205 | mpbird 247 |
. 2
inf |
207 | 66 | a1i 11 |
. . . . 5
|
208 | | nfv 1843 |
. . . . . 6
|
209 | 11 | ffvelrnda 6359 |
. . . . . 6
|
210 | 13 | ffvelrnda 6359 |
. . . . . . 7
|
211 | 210 | rexrd 10089 |
. . . . . 6
|
212 | 208, 209,
211 | hoissrrn2 40792 |
. . . . 5
|
213 | 207, 212 | eqsstrd 3639 |
. . . 4
|
214 | 9, 177, 213, 1 | ovnn0val 40765 |
. . 3
voln* inf |
215 | 214 | eqcomd 2628 |
. 2
inf voln* |
216 | 206, 215 | breqtrd 4679 |
1
voln* |