hoidmvle - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hoidmvle		Structured version Visualization version Unicode version

Theorem hoidmvle 38540

Description: The dimensional volume of a n-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)

**Hypotheses**
Ref	Expression
hoidmvle.l
hoidmvle.x
hoidmvle.a
hoidmvle.b
hoidmvle.c
hoidmvle.d
hoidmvle.s

**Assertion**
Ref	Expression
hoidmvle	Σ^{^}

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem hoidmvle Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hoidmvle.s	. 2
2		hoidmvle.d	. . . 4
3		ovex 6336	. . . . . . 7
4		nnex 10637	. . . . . . 7
5	3, 4	pm3.2i 462	. . . . . 6 $/\$
6	5	a1i 11	. . . . 5 $/\$
7		elmapg 7503	. . . . 5 $/\$
8	6, 7	syl 17	. . . 4
9	2, 8	mpbird 240	. . 3
10		hoidmvle.c	. . . . 5
11		elmapg 7503	. . . . . 6 $/\$
12	6, 11	syl 17	. . . . 5
13	10, 12	mpbird 240	. . . 4
14		hoidmvle.b	. . . . . 6
15		reex 9648	. . . . . . . . 9
16	15	a1i 11	. . . . . . . 8
17		hoidmvle.x	. . . . . . . 8
18	16, 17	jca 541	. . . . . . 7 $/\$
19		elmapg 7503	. . . . . . 7 $/\$
20	18, 19	syl 17	. . . . . 6
21	14, 20	mpbird 240	. . . . 5
22		hoidmvle.a	. . . . . . 7
23		elmapg 7503	. . . . . . . 8 $/\$
24	18, 23	syl 17	. . . . . . 7
25	22, 24	mpbird 240	. . . . . 6
26		oveq2 6316	. . . . . . . . . 10
27	26	eleq2d 2534	. . . . . . . . 9
28	26	eleq2d 2534	. . . . . . . . . . 11
29	26	oveq1d 6323	. . . . . . . . . . . . . 14
30	29	eleq2d 2534	. . . . . . . . . . . . 13
31	29	eleq2d 2534	. . . . . . . . . . . . . . 15
32		ixpeq1 7551	. . . . . . . . . . . . . . . . 17
33		ixpeq1 7551	. . . . . . . . . . . . . . . . . 18
34	33	iuneq2d 4296	. . . . . . . . . . . . . . . . 17
35	32, 34	sseq12d 3447	. . . . . . . . . . . . . . . 16
36		fveq2 5879	. . . . . . . . . . . . . . . . . 18
37	36	oveqd 6325	. . . . . . . . . . . . . . . . 17
38	36	oveqd 6325	. . . . . . . . . . . . . . . . . . 19
39	38	mpteq2dv 4483	. . . . . . . . . . . . . . . . . 18
40	39	fveq2d 5883	. . . . . . . . . . . . . . . . 17 Σ^{^} Σ^{^}
41	37, 40	breq12d 4408	. . . . . . . . . . . . . . . 16 Σ^{^} Σ^{^}
42	35, 41	imbi12d 327	. . . . . . . . . . . . . . 15 Σ^{^} Σ^{^}
43	31, 42	imbi12d 327	. . . . . . . . . . . . . 14 Σ^{^} Σ^{^}
44	43	ralbidv2 2827	. . . . . . . . . . . . 13 Σ^{^} Σ^{^}
45	30, 44	imbi12d 327	. . . . . . . . . . . 12 Σ^{^} Σ^{^}
46	45	ralbidv2 2827	. . . . . . . . . . 11 Σ^{^} Σ^{^}
47	28, 46	imbi12d 327	. . . . . . . . . 10 Σ^{^} Σ^{^}
48	47	ralbidv2 2827	. . . . . . . . 9 Σ^{^} Σ^{^}
49	27, 48	imbi12d 327	. . . . . . . 8 Σ^{^} Σ^{^}
50	49	ralbidv2 2827	. . . . . . 7 Σ^{^} Σ^{^}
51		oveq2 6316	. . . . . . . . . 10
52	51	eleq2d 2534	. . . . . . . . 9
53	51	eleq2d 2534	. . . . . . . . . . 11
54	51	oveq1d 6323	. . . . . . . . . . . . . 14
55	54	eleq2d 2534	. . . . . . . . . . . . 13
56	54	eleq2d 2534	. . . . . . . . . . . . . . 15
57		ixpeq1 7551	. . . . . . . . . . . . . . . . 17
58		ixpeq1 7551	. . . . . . . . . . . . . . . . . 18
59	58	iuneq2d 4296	. . . . . . . . . . . . . . . . 17
60	57, 59	sseq12d 3447	. . . . . . . . . . . . . . . 16
61		fveq2 5879	. . . . . . . . . . . . . . . . . 18
62	61	oveqd 6325	. . . . . . . . . . . . . . . . 17
63	61	oveqd 6325	. . . . . . . . . . . . . . . . . . 19
64	63	mpteq2dv 4483	. . . . . . . . . . . . . . . . . 18
65	64	fveq2d 5883	. . . . . . . . . . . . . . . . 17 Σ^{^} Σ^{^}
66	62, 65	breq12d 4408	. . . . . . . . . . . . . . . 16 Σ^{^} Σ^{^}
67	60, 66	imbi12d 327	. . . . . . . . . . . . . . 15 Σ^{^} Σ^{^}
68	56, 67	imbi12d 327	. . . . . . . . . . . . . 14 Σ^{^} Σ^{^}
69	68	ralbidv2 2827	. . . . . . . . . . . . 13 Σ^{^} Σ^{^}
70	55, 69	imbi12d 327	. . . . . . . . . . . 12 Σ^{^} Σ^{^}
71	70	ralbidv2 2827	. . . . . . . . . . 11 Σ^{^} Σ^{^}
72	53, 71	imbi12d 327	. . . . . . . . . 10 Σ^{^} Σ^{^}
73	72	ralbidv2 2827	. . . . . . . . 9 Σ^{^} Σ^{^}
74	52, 73	imbi12d 327	. . . . . . . 8 Σ^{^} Σ^{^}
75	74	ralbidv2 2827	. . . . . . 7 Σ^{^} Σ^{^}
76		oveq2 6316	. . . . . . . . . 10
77	76	eleq2d 2534	. . . . . . . . 9
78	76	eleq2d 2534	. . . . . . . . . . 11
79	76	oveq1d 6323	. . . . . . . . . . . . . 14
80	79	eleq2d 2534	. . . . . . . . . . . . 13
81	79	eleq2d 2534	. . . . . . . . . . . . . . 15
82		ixpeq1 7551	. . . . . . . . . . . . . . . . 17
83		ixpeq1 7551	. . . . . . . . . . . . . . . . . 18
84	83	iuneq2d 4296	. . . . . . . . . . . . . . . . 17
85	82, 84	sseq12d 3447	. . . . . . . . . . . . . . . 16
86		fveq2 5879	. . . . . . . . . . . . . . . . . 18
87	86	oveqd 6325	. . . . . . . . . . . . . . . . 17
88	86	oveqd 6325	. . . . . . . . . . . . . . . . . . 19
89	88	mpteq2dv 4483	. . . . . . . . . . . . . . . . . 18
90	89	fveq2d 5883	. . . . . . . . . . . . . . . . 17 Σ^{^} Σ^{^}
91	87, 90	breq12d 4408	. . . . . . . . . . . . . . . 16 Σ^{^} Σ^{^}
92	85, 91	imbi12d 327	. . . . . . . . . . . . . . 15 Σ^{^} Σ^{^}
93	81, 92	imbi12d 327	. . . . . . . . . . . . . 14 Σ^{^} Σ^{^}
94	93	ralbidv2 2827	. . . . . . . . . . . . 13 Σ^{^} Σ^{^}
95	80, 94	imbi12d 327	. . . . . . . . . . . 12 Σ^{^} Σ^{^}
96	95	ralbidv2 2827	. . . . . . . . . . 11 Σ^{^} Σ^{^}
97	78, 96	imbi12d 327	. . . . . . . . . 10 Σ^{^} Σ^{^}
98	97	ralbidv2 2827	. . . . . . . . 9 Σ^{^} Σ^{^}
99	77, 98	imbi12d 327	. . . . . . . 8 Σ^{^} Σ^{^}
100	99	ralbidv2 2827	. . . . . . 7 Σ^{^} Σ^{^}
101		oveq2 6316	. . . . . . . . . 10
102	101	eleq2d 2534	. . . . . . . . 9
103	101	eleq2d 2534	. . . . . . . . . . 11
104	101	oveq1d 6323	. . . . . . . . . . . . . 14
105	104	eleq2d 2534	. . . . . . . . . . . . 13
106	104	eleq2d 2534	. . . . . . . . . . . . . . 15
107		ixpeq1 7551	. . . . . . . . . . . . . . . . 17
108		ixpeq1 7551	. . . . . . . . . . . . . . . . . 18
109	108	iuneq2d 4296	. . . . . . . . . . . . . . . . 17
110	107, 109	sseq12d 3447	. . . . . . . . . . . . . . . 16
111		fveq2 5879	. . . . . . . . . . . . . . . . . 18
112	111	oveqd 6325	. . . . . . . . . . . . . . . . 17
113	111	oveqd 6325	. . . . . . . . . . . . . . . . . . 19
114	113	mpteq2dv 4483	. . . . . . . . . . . . . . . . . 18
115	114	fveq2d 5883	. . . . . . . . . . . . . . . . 17 Σ^{^} Σ^{^}
116	112, 115	breq12d 4408	. . . . . . . . . . . . . . . 16 Σ^{^} Σ^{^}
117	110, 116	imbi12d 327	. . . . . . . . . . . . . . 15 Σ^{^} Σ^{^}
118	106, 117	imbi12d 327	. . . . . . . . . . . . . 14 Σ^{^} Σ^{^}
119	118	ralbidv2 2827	. . . . . . . . . . . . 13 Σ^{^} Σ^{^}
120	105, 119	imbi12d 327	. . . . . . . . . . . 12 Σ^{^} Σ^{^}
121	120	ralbidv2 2827	. . . . . . . . . . 11 Σ^{^} Σ^{^}
122	103, 121	imbi12d 327	. . . . . . . . . 10 Σ^{^} Σ^{^}
123	122	ralbidv2 2827	. . . . . . . . 9 Σ^{^} Σ^{^}
124	102, 123	imbi12d 327	. . . . . . . 8 Σ^{^} Σ^{^}
125	124	ralbidv2 2827	. . . . . . 7 Σ^{^} Σ^{^}
126		hoidmvle.l	. . . . . . . . . . . . . . . 16
127		fveq1 5878	. . . . . . . . . . . . . . . . . . . . . 22
128	127	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . 21
129	128	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20
130	129	prodeq2ad 37769	. . . . . . . . . . . . . . . . . . 19
131	130	ifeq2d 3891	. . . . . . . . . . . . . . . . . 18
132		fveq1 5878	. . . . . . . . . . . . . . . . . . . . . 22
133	132	oveq2d 6324	. . . . . . . . . . . . . . . . . . . . 21
134	133	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20
135	134	prodeq2ad 37769	. . . . . . . . . . . . . . . . . . 19
136	135	ifeq2d 3891	. . . . . . . . . . . . . . . . . 18
137	131, 136	cbvmpt2v 6390	. . . . . . . . . . . . . . . . 17
138	137	mpteq2i 4479	. . . . . . . . . . . . . . . 16
139	126, 138	eqtri 2493	. . . . . . . . . . . . . . 15
140		elmapi 7511	. . . . . . . . . . . . . . . 16
141	140	adantr 472	. . . . . . . . . . . . . . 15 $/\$
142		elmapi 7511	. . . . . . . . . . . . . . . 16
143	142	adantl 473	. . . . . . . . . . . . . . 15 $/\$
144	139, 141, 143	hoidmv0val 38523	. . . . . . . . . . . . . 14 $/\$
145	144	ad5ant23 1270	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
146		nfv 1769	. . . . . . . . . . . . . . 15 $/\$
147	4	a1i 11	. . . . . . . . . . . . . . 15 $/\$
148		icossicc 11746	. . . . . . . . . . . . . . . 16
149		0fin 7817	. . . . . . . . . . . . . . . . . 18
150	149	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
151		ovex 6336	. . . . . . . . . . . . . . . . . . . . 21
152	151	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
153	4	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
154		simpl 464	. . . . . . . . . . . . . . . . . . . 20 $/\$
155		simpr 468	. . . . . . . . . . . . . . . . . . . 20 $/\$
156	152, 153, 154, 155	fvmap 37546	. . . . . . . . . . . . . . . . . . 19 $/\$
157		elmapi 7511	. . . . . . . . . . . . . . . . . . 19
158	156, 157	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$
159	158	adantlr 729	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
160	151	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
161	4	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$
162		simpl 464	. . . . . . . . . . . . . . . . . . . 20 $/\$
163		simpr 468	. . . . . . . . . . . . . . . . . . . 20 $/\$
164	160, 161, 162, 163	fvmap 37546	. . . . . . . . . . . . . . . . . . 19 $/\$
165		elmapi 7511	. . . . . . . . . . . . . . . . . . 19
166	164, 165	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$
167	166	adantll 728	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
168	126, 150, 159, 167	hoidmvcl 38522	. . . . . . . . . . . . . . . 16 $/\$ $/\$
169	148, 168	sseldi 3416	. . . . . . . . . . . . . . 15 $/\$ $/\$
170	146, 147, 169	sge0ge0mpt 38394	. . . . . . . . . . . . . 14 $/\$ Σ^{^}
171	170	adantll 728	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Σ^{^}
172	145, 171	eqbrtrd 4416	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Σ^{^}
173	172	a1d 25	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Σ^{^}
174	173	ralrimiva 2809	. . . . . . . . . 10 $/\$ $/\$ $/\$ Σ^{^}
175	174	ralrimiva 2809	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
176	175	ralrimiva 2809	. . . . . . . 8 $/\$ Σ^{^}
177	176	ralrimiva 2809	. . . . . . 7 Σ^{^}
178		simpl 464	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$ Σ^{^} $/\$ $/\$ $\$
179	128	ixpeq2dv 7556	. . . . . . . . . . . . . . . . . 18
180	179	sseq1d 3445	. . . . . . . . . . . . . . . . 17
181		oveq1 6315	. . . . . . . . . . . . . . . . . 18
182	181	breq1d 4405	. . . . . . . . . . . . . . . . 17 Σ^{^} Σ^{^}
183	180, 182	imbi12d 327	. . . . . . . . . . . . . . . 16 Σ^{^} Σ^{^}
184	183	ralbidv 2829	. . . . . . . . . . . . . . 15 Σ^{^} Σ^{^}
185	184	ralbidv 2829	. . . . . . . . . . . . . 14 Σ^{^} Σ^{^}
186	185	ralbidv 2829	. . . . . . . . . . . . 13 Σ^{^} Σ^{^}
187	133	ixpeq2dv 7556	. . . . . . . . . . . . . . . . . . . 20
188	187	sseq1d 3445	. . . . . . . . . . . . . . . . . . 19
189		oveq2 6316	. . . . . . . . . . . . . . . . . . . 20
190	189	breq1d 4405	. . . . . . . . . . . . . . . . . . 19 Σ^{^} Σ^{^}
191	188, 190	imbi12d 327	. . . . . . . . . . . . . . . . . 18 Σ^{^} Σ^{^}
192	191	ralbidv 2829	. . . . . . . . . . . . . . . . 17 Σ^{^}