hoidmvlelem3 - Mathbox for Glauco Siliprandi

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

Theorem hoidmvlelem3 40811

Description: This is the contradiction proven in step (d) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)

**Hypotheses**
Ref	Expression
hoidmvlelem3.l
hoidmvlelem3.x
hoidmvlelem3.y
hoidmvlelem3.z	$\$
hoidmvlelem3.w
hoidmvlelem3.a
hoidmvlelem3.b
hoidmvlelem3.lt	$/\$
hoidmvlelem3.f
hoidmvlelem3.c
hoidmvlelem3.j
hoidmvlelem3.d
hoidmvlelem3.k
hoidmvlelem3.r	Σ^{^}
hoidmvlelem3.h
hoidmvlelem3.g
hoidmvlelem3.e
hoidmvlelem3.u	Σ^{^}
hoidmvlelem3.s
hoidmvlelem3.sb
hoidmvlelem3.p
hoidmvlelem3.i	Σ^{^}
hoidmvlelem3.i2
hoidmvlelem3.o

**Assertion**
Ref	Expression
hoidmvlelem3

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem hoidmvlelem3 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1nn 11031	. . . . 5
2	1	a1i 11	. . . 4 $/\$
3		0le0 11110	. . . . . 6
4	3	a1i 11	. . . . 5 $/\$
5		hoidmvlelem3.g	. . . . . . . 8
6	5	a1i 11	. . . . . . 7 $/\$
7		fveq2 6191	. . . . . . . . 9
8		reseq2 5391	. . . . . . . . . 10
9		res0 5400	. . . . . . . . . . 11
10	9	a1i 11	. . . . . . . . . 10
11	8, 10	eqtrd 2656	. . . . . . . . 9
12		reseq2 5391	. . . . . . . . . 10
13		res0 5400	. . . . . . . . . . 11
14	13	a1i 11	. . . . . . . . . 10
15	12, 14	eqtrd 2656	. . . . . . . . 9
16	7, 11, 15	oveq123d 6671	. . . . . . . 8
17	16	adantl 482	. . . . . . 7 $/\$
18		hoidmvlelem3.l	. . . . . . . 8
19		f0 6086	. . . . . . . . 9
20	19	a1i 11	. . . . . . . 8 $/\$
21	18, 20, 20	hoidmv0val 40797	. . . . . . 7 $/\$
22	6, 17, 21	3eqtrd 2660	. . . . . 6 $/\$
23		nfcvd 2765	. . . . . . . . . . 11
24		nfv 1843	. . . . . . . . . . 11
25		simpr 477	. . . . . . . . . . . 12 $/\$
26	25	fveq2d 6195	. . . . . . . . . . 11 $/\$
27		1red 10055	. . . . . . . . . . 11
28		rge0ssre 12280	. . . . . . . . . . . . 13
29		id 22	. . . . . . . . . . . . . 14
30	1	a1i 11	. . . . . . . . . . . . . 14
31	1	elexi 3213	. . . . . . . . . . . . . . 15
32		eleq1 2689	. . . . . . . . . . . . . . . . 17
33	32	anbi2d 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$
34		fveq2 6191	. . . . . . . . . . . . . . . . 17
35	34	eleq1d 2686	. . . . . . . . . . . . . . . 16
36	33, 35	imbi12d 334	. . . . . . . . . . . . . . 15 $/\$ $/\$
37		id 22	. . . . . . . . . . . . . . . . . 18
38		ovexd 6680	. . . . . . . . . . . . . . . . . 18
39		hoidmvlelem3.p	. . . . . . . . . . . . . . . . . . 19
40	39	fvmpt2 6291	. . . . . . . . . . . . . . . . . 18 $/\$
41	37, 38, 40	syl2anc 693	. . . . . . . . . . . . . . . . 17
42	41	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
43		hoidmvlelem3.x	. . . . . . . . . . . . . . . . . . . 20
44		hoidmvlelem3.w	. . . . . . . . . . . . . . . . . . . . . 22
45	44	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
46		hoidmvlelem3.y	. . . . . . . . . . . . . . . . . . . . . 22
47		hoidmvlelem3.z	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
48	47	eldifad 3586	. . . . . . . . . . . . . . . . . . . . . . 23
49		snssi 4339	. . . . . . . . . . . . . . . . . . . . . . 23
50	48, 49	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
51	46, 50	unssd 3789	. . . . . . . . . . . . . . . . . . . . 21
52	45, 51	eqsstrd 3639	. . . . . . . . . . . . . . . . . . . 20
53	43, 52	ssfid 8183	. . . . . . . . . . . . . . . . . . 19
54		ssun1 3776	. . . . . . . . . . . . . . . . . . . . 21
55	44	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . 21
56	54, 55	sseqtri 3637	. . . . . . . . . . . . . . . . . . . 20
57	56	a1i 11	. . . . . . . . . . . . . . . . . . 19
58	53, 57	ssfid 8183	. . . . . . . . . . . . . . . . . 18
59	58	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
60		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . 23
61	60	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
62		hoidmvlelem3.c	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
63	62	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
64		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . . . . 26
65	63, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
66	54, 44	sseqtr4i 3638	. . . . . . . . . . . . . . . . . . . . . . . . . 26
67	66	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
68	65, 67	fssresd 6071	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
69		reex 10027	. . . . . . . . . . . . . . . . . . . . . . . . . 26
70	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
71	53, 57	ssexd 4805	. . . . . . . . . . . . . . . . . . . . . . . . . 26
72	71	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
73	70, 72	elmapd 7871	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
74	68, 73	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
75	74	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
76	61, 75	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
77		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . 23
78	77	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
79		0red 10041	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
80		hoidmvlelem3.f	. . . . . . . . . . . . . . . . . . . . . . . . 25
81	79, 80	fmptd 6385	. . . . . . . . . . . . . . . . . . . . . . . 24
82	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
83	82, 58	elmapd 7871	. . . . . . . . . . . . . . . . . . . . . . . 24
84	81, 83	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . 23
85	84	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
86	78, 85	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
87	76, 86	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . 20 $/\$
88		hoidmvlelem3.j	. . . . . . . . . . . . . . . . . . . 20
89	87, 88	fmptd 6385	. . . . . . . . . . . . . . . . . . 19
90	89	ffvelrnda 6359	. . . . . . . . . . . . . . . . . 18 $/\$
91		elmapi 7879	. . . . . . . . . . . . . . . . . 18
92	90, 91	syl 17	. . . . . . . . . . . . . . . . 17 $/\$
93		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . 23
94	93	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
95		hoidmvlelem3.d	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
96	95	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
97		elmapi 7879	. . . . . . . . . . . . . . . . . . . . . . . . . 26
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
99	98, 67	fssresd 6071	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
100	70, 72	elmapd 7871	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
101	99, 100	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
102	101	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
103	94, 102	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
104		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . 23
105	104	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
106	105, 85	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	103, 106	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . 20 $/\$
108		hoidmvlelem3.k	. . . . . . . . . . . . . . . . . . . 20
109	107, 108	fmptd 6385	. . . . . . . . . . . . . . . . . . 19
110	109	ffvelrnda 6359	. . . . . . . . . . . . . . . . . 18 $/\$
111		elmapi 7879	. . . . . . . . . . . . . . . . . 18
112	110, 111	syl 17	. . . . . . . . . . . . . . . . 17 $/\$
113	18, 59, 92, 112	hoidmvcl 40796	. . . . . . . . . . . . . . . 16 $/\$
114	42, 113	eqeltrd 2701	. . . . . . . . . . . . . . 15 $/\$
115	31, 36, 114	vtocl 3259	. . . . . . . . . . . . . 14 $/\$
116	29, 30, 115	syl2anc 693	. . . . . . . . . . . . 13
117	28, 116	sseldi 3601	. . . . . . . . . . . 12
118	117	recnd 10068	. . . . . . . . . . 11
119	23, 24, 26, 27, 118	sumsnd 39185	. . . . . . . . . 10
120	119	adantr 481	. . . . . . . . 9 $/\$
121		fveq2 6191	. . . . . . . . . . . . 13
122		fveq2 6191	. . . . . . . . . . . . 13
123	121, 122	oveq12d 6668	. . . . . . . . . . . 12
124		ovex 6678	. . . . . . . . . . . 12
125	123, 39, 124	fvmpt 6282	. . . . . . . . . . 11
126	1, 125	ax-mp 5	. . . . . . . . . 10
127	126	a1i 11	. . . . . . . . 9 $/\$
128	7	oveqd 6667	. . . . . . . . . . 11
129	128	adantl 482	. . . . . . . . . 10 $/\$
130	121	feq1d 6030	. . . . . . . . . . . . . . . 16
131	33, 130	imbi12d 334	. . . . . . . . . . . . . . 15 $/\$ $/\$
132	68	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
133	61	feq1d 6030	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
134	132, 133	mpbird 247	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
135	81	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
136	78	feq1d 6030	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
137	135, 136	mpbird 247	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
138	134, 137	pm2.61dan 832	. . . . . . . . . . . . . . . 16 $/\$
139		simpr 477	. . . . . . . . . . . . . . . . . 18 $/\$
140		fvex 6201	. . . . . . . . . . . . . . . . . . . . 21
141	140	resex 5443	. . . . . . . . . . . . . . . . . . . 20
142	61, 141	syl6eqel 2709	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
143	84	elexd 3214	. . . . . . . . . . . . . . . . . . . . . 22
144	143	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
145	144	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
146	78, 145	eqeltrd 2701	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
147	142, 146	pm2.61dan 832	. . . . . . . . . . . . . . . . . 18 $/\$
148	88	fvmpt2 6291	. . . . . . . . . . . . . . . . . 18 $/\$
149	139, 147, 148	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$
150	149	feq1d 6030	. . . . . . . . . . . . . . . 16 $/\$
151	138, 150	mpbird 247	. . . . . . . . . . . . . . 15 $/\$
152	31, 131, 151	vtocl 3259	. . . . . . . . . . . . . 14 $/\$
153	29, 30, 152	syl2anc 693	. . . . . . . . . . . . 13
154	153	adantr 481	. . . . . . . . . . . 12 $/\$
155		id 22	. . . . . . . . . . . . . . 15
156	155	eqcomd 2628	. . . . . . . . . . . . . 14
157	156	feq2d 6031	. . . . . . . . . . . . 13
158	157	adantl 482	. . . . . . . . . . . 12 $/\$
159	154, 158	mpbird 247	. . . . . . . . . . 11 $/\$
160	122	feq1d 6030	. . . . . . . . . . . . . . . 16
161	33, 160	imbi12d 334	. . . . . . . . . . . . . . 15 $/\$ $/\$
162	31, 161, 112	vtocl 3259	. . . . . . . . . . . . . 14 $/\$
163	29, 30, 162	syl2anc 693	. . . . . . . . . . . . 13
164	163	adantr 481	. . . . . . . . . . . 12 $/\$
165	156	feq2d 6031	. . . . . . . . . . . . 13
166	165	adantl 482	. . . . . . . . . . . 12 $/\$
167	164, 166	mpbird 247	. . . . . . . . . . 11 $/\$
168	18, 159, 167	hoidmv0val 40797	. . . . . . . . . 10 $/\$
169	129, 168	eqtrd 2656	. . . . . . . . 9 $/\$
170	120, 127, 169	3eqtrd 2660	. . . . . . . 8 $/\$
171	170	oveq2d 6666	. . . . . . 7 $/\$
172		hoidmvlelem3.e	. . . . . . . . . . . 12
173	172	rpred 11872	. . . . . . . . . . 11
174	27, 173	readdcld 10069	. . . . . . . . . 10
175	174	recnd 10068	. . . . . . . . 9
176	175	mul01d 10235	. . . . . . . 8
177	176	adantr 481	. . . . . . 7 $/\$
178		eqidd 2623	. . . . . . 7 $/\$
179	171, 177, 178	3eqtrd 2660	. . . . . 6 $/\$
180	22, 179	breq12d 4666	. . . . 5 $/\$
181	4, 180	mpbird 247	. . . 4 $/\$
182		oveq2 6658	. . . . . . . . 9
183	1	nnzi 11401	. . . . . . . . . . 11
184		fzsn 12383	. . . . . . . . . . 11
185	183, 184	ax-mp 5	. . . . . . . . . 10
186	185	a1i 11	. . . . . . . . 9
187	182, 186	eqtrd 2656	. . . . . . . 8
188	187	sumeq1d 14431	. . . . . . 7
189	188	oveq2d 6666	. . . . . 6
190	189	breq2d 4665	. . . . 5
191	190	rspcev 3309	. . . 4 $/\$
192	2, 181, 191	syl2anc 693	. . 3 $/\$
193		simpl 473	. . . 4 $/\$
194		neqne 2802	. . . . 5
195	194	adantl 482	. . . 4 $/\$
196		nfv 1843	. . . . . 6 $/\$
197	183	a1i 11	. . . . . 6 $/\$
198		nnuz 11723	. . . . . 6
199	114	adantlr 751	. . . . . 6 $/\$ $/\$
200		hoidmvlelem3.a	. . . . . . . . . . . 12
201	66	a1i 11	. . . . . . . . . . . 12
202	200, 201	fssresd 6071	. . . . . . . . . . 11
203		hoidmvlelem3.b	. . . . . . . . . . . 12
204	203, 201	fssresd 6071	. . . . . . . . . . 11
205	18, 58, 202, 204	hoidmvcl 40796	. . . . . . . . . 10
206	28, 205	sseldi 3601	. . . . . . . . 9
207	5, 206	syl5eqel 2705	. . . . . . . 8
208		0red 10041	. . . . . . . . 9
209		1rp 11836	. . . . . . . . . . . . 13
210	209	a1i 11	. . . . . . . . . . . 12
211	210, 172	jca 554	. . . . . . . . . . 11 $/\$
212		rpaddcl 11854	. . . . . . . . . . 11 $/\$
213	211, 212	syl 17	. . . . . . . . . 10
214		rpgt0 11844	. . . . . . . . . 10
215	213, 214	syl 17	. . . . . . . . 9
216	208, 215	gtned 10172	. . . . . . . 8
217	207, 174, 216	redivcld 10853	. . . . . . 7
218	217	adantr 481	. . . . . 6 $/\$
219	217	ltpnfd 11955	. . . . . . . . . 10
220	219	adantr 481	. . . . . . . . 9 $/\$ Σ^{^}
221		id 22	. . . . . . . . . . 11 Σ^{^} Σ^{^}
222	221	eqcomd 2628	. . . . . . . . . 10 Σ^{^} Σ^{^}
223	222	adantl 482	. . . . . . . . 9 $/\$ Σ^{^} Σ^{^}
224	220, 223	breqtrd 4679	. . . . . . . 8 $/\$ Σ^{^} Σ^{^}
225	224	adantlr 751	. . . . . . 7 $/\$ $/\$ Σ^{^} Σ^{^}
226		simpl 473	. . . . . . . 8 $/\$ $/\$ Σ^{^} $/\$
227		simpr 477	. . . . . . . . . 10 $/\$ Σ^{^} Σ^{^}
228		nnex 11026	. . . . . . . . . . . 12
229	228	a1i 11	. . . . . . . . . . 11 $/\$ Σ^{^}
230		icossicc 12260	. . . . . . . . . . . . . 14
231	230, 114	sseldi 3601	. . . . . . . . . . . . 13 $/\$
232		eqid 2622	. . . . . . . . . . . . 13
233	231, 232	fmptd 6385	. . . . . . . . . . . 12
234	233	adantr 481	. . . . . . . . . . 11 $/\$ Σ^{^}
235	229, 234	sge0repnf 40603	. . . . . . . . . 10 $/\$ Σ^{^} Σ^{^} Σ^{^}
236	227, 235	mpbird 247	. . . . . . . . 9 $/\$ Σ^{^} Σ^{^}
237	236	adantlr 751	. . . . . . . 8 $/\$ $/\$ Σ^{^} Σ^{^}
238	218	adantr 481	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
239	207	adantr 481	. . . . . . . . . 10 $/\$ Σ^{^}
240	239	adantlr 751	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
241		simpr 477	. . . . . . . . 9 $/\$ $/\$ Σ^{^} Σ^{^}
242	27, 172	ltaddrpd 11905	. . . . . . . . . . . 12
243	242	adantr 481	. . . . . . . . . . 11 $/\$
244	58	adantr 481	. . . . . . . . . . . . . . 15 $/\$
245		simpr 477	. . . . . . . . . . . . . . 15 $/\$
246	202	adantr 481	. . . . . . . . . . . . . . 15 $/\$
247	204	adantr 481	. . . . . . . . . . . . . . 15 $/\$
248	18, 244, 245, 246, 247	hoidmvn0val 40798	. . . . . . . . . . . . . 14 $/\$
249	5	a1i 11	. . . . . . . . . . . . . 14 $/\$
250		fvres 6207	. . . . . . . . . . . . . . . . . . . . 21
251		fvres 6207	. . . . . . . . . . . . . . . . . . . . 21
252	250, 251	oveq12d 6668	. . . . . . . . . . . . . . . . . . . 20
253	252	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19
254	253	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
255	200	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
256		elun1 3780	. . . . . . . . . . . . . . . . . . . . . 22
257	256, 44	syl6eleqr 2712	. . . . . . . . . . . . . . . . . . . . 21
258	257	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
259	255, 258	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 $/\$
260	203	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
261	260, 258	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 $/\$
262		volico 40200	. . . . . . . . . . . . . . . . . . 19 $/\$
263	259, 261, 262	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$
264		hoidmvlelem3.lt	. . . . . . . . . . . . . . . . . . . 20 $/\$
265	258, 264	syldan 487	. . . . . . . . . . . . . . . . . . 19 $/\$
266	265	iftrued 4094	. . . . . . . . . . . . . . . . . 18 $/\$
267	254, 263, 266	3eqtrd 2660	. . . . . . . . . . . . . . . . 17 $/\$
268	267	prodeq2dv 14653	. . . . . . . . . . . . . . . 16
269	268	eqcomd 2628	. . . . . . . . . . . . . . 15
270	269	adantr 481	. . . . . . . . . . . . . 14 $/\$
271	248, 249, 270	3eqtr4d 2666	. . . . . . . . . . . . 13 $/\$
272		difrp 11868	. . . . . . . . . . . . . . . . 17 $/\$
273	259, 261, 272	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$
274	265, 273	mpbid 222	. . . . . . . . . . . . . . 15 $/\$
275	58, 274	fprodrpcl 14686	. . . . . . . . . . . . . 14
276	275	adantr 481	. . . . . . . . . . . . 13 $/\$
277	271, 276	eqeltrd 2701	. . . . . . . . . . . 12 $/\$
278	213	adantr 481	. . . . . . . . . . . 12 $/\$
279	277, 278	ltdivgt1 39572	. . . . . . . . . . 11 $/\$
280	243, 279	mpbid 222	. . . . . . . . . 10 $/\$
281	280	adantr 481	. . . . . . . . 9 $/\$ $/\$ Σ^{^}
282		hoidmvlelem3.i2	. . . . . . . . . . . . . . . . . . . . 21
283	282	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
284		fvexd 6203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
285		hoidmvlelem3.s	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
286	285	elexd 3214	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
287	284, 286	ifcld 4131	. . . . . . . . . . . . . . . . . . . . . . . . . 26
288	287	ralrimivw 2967	. . . . . . . . . . . . . . . . . . . . . . . . 25
289	288	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
290		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . 25
291	290	fnmpt 6020	. . . . . . . . . . . . . . . . . . . . . . . 24
292	289, 291	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
293		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
294		mptexg 6484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
295	53, 294	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
296	295	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
297		hoidmvlelem3.o	. . . . . . . . . . . . . . . . . . . . . . . . . 26
298	297	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
299	293, 296, 298	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
300	299	fneq1d 5981	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
301	292, 300	mpbird 247	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
302		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . 24
303		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . 25
304		nfixp1 7928	. . . . . . . . . . . . . . . . . . . . . . . . 25
305	303, 304	nfel 2777	. . . . . . . . . . . . . . . . . . . . . . . 24
306	302, 305	nfan 1828	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
307	299	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
308	307	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
309		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
310	287	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
311	290	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
312	309, 310, 311	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
313	312	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
314	308, 313	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
315		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
316	315	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
317		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
318	317	elixp 7915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
319	318	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
320	319	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
321		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
322		rspa 2930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
323	320, 321, 322	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
324	323	ad4ant24 1298	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
325	316, 324	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
326		snidg 4206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $\$
327	47, 326	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
328		elun2 3781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
329	327, 328	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
330	55	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
331	329, 330	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
332	200, 331	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
333	332	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
334	203, 331	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
335	334	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
336		iccssxr 12256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
337		hoidmvlelem3.u	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Σ^{^}
338		ssrab2 3687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Σ^{^}
339	337, 338	eqsstri 3635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
340	339, 285	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
341	336, 340	sseldi 3601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
342		iccgelb 12230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
343	333, 335, 340, 342	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
344		hoidmvlelem3.sb	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
345	333, 335, 341, 343, 344	elicod 12224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
346	345	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
347		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
348	347	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
349	44	eleq2i 2693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
350	349	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
351	350	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
352		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
353		elunnel1 3754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
354	351, 352, 353	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
355		elsni 4194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
356	354, 355	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
357		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
358		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
359	357, 358	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
360	356, 359	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
361	360	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
362	348, 361	eleq12d 2695	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
363	346, 362	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
364	363	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
365	325, 364	pm2.61dan 832	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
366	314, 365	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
367	366	ex 450	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
368	306, 367	ralrimi 2957	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
369	301, 368	jca 554	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
370		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22
371	370	elixp 7915	. . . . . . . . . . . . . . . . . . . . 21 $/\$
372	369, 371	sylibr 224	. . . . . . . . . . . . . . . . . . . 20 $/\$
373	283, 372	sseldd 3604	. . . . . . . . . . . . . . . . . . 19 $/\$
374		eliun 4524	. . . . . . . . . . . . . . . . . . 19
375	373, 374	sylib 208	. . . . . . . . . . . . . . . . . 18 $/\$
376		ixpfn 7914	. . . . . . . . . . . . . . . . . . . . . . . 24
377	376	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
378	377	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
379		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . . 25
380	306, 379	nfan 1828	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
381		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . 25
382		nfixp1 7928	. . . . . . . . . . . . . . . . . . . . . . . . 25
383	381, 382	nfel 2777	. . . . . . . . . . . . . . . . . . . . . . . 24
384	380, 383	nfan 1828	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
385	307	3adant3 1081	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
386	287	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
387	258, 386, 311	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
388	387	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
389	315	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
390	385, 388, 389	3eqtrrd 2661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
391	390	ad5ant125 1312	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
392		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
393	370	elixp 7915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
394	392, 393	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
395	394	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
396	257	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
397		rspa 2930	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
398	395, 396, 397	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
399	398	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
400	391, 399	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
401	29	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
402	37	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
403	299	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
404		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
405		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
406		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
407	405, 406	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
408	407	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
409		fvexd 6203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
410	409, 286	ifcld 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
411	404, 408, 331, 410	fvmptd 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
412	411	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
413	47	eldifbd 3587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
414	413	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
415	414	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
416	403, 412, 415	3eqtrrd 2661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
417	416	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
418	401, 331	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
419	393	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
420	419	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
421		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
422		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
423		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
424	422, 423	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
425	421, 424	eleq12d 2695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
426	425	rspcva 3307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
427	418, 420, 426	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
428	417, 427	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$
429	149	3adant3 1081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
430	60	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
431	429, 430	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
432	431	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
433	401, 402, 428, 432	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
434	433	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
435		fvres 6207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
436	435	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
437	434, 436	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
438	107	elexd 3214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
439	108	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
440	139, 438, 439	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
441	440	3adant3 1081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
442	93	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
443	441, 442	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
444	443	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
445	401, 402, 428, 444	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
446	445	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
447		fvres 6207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
448	447	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
449	446, 448	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
450	437, 449	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
451	450	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
452	400, 451	eleqtrd 2703	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
453	452	ex 450	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
454	384, 453	ralrimi 2957	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
455	378, 454	jca 554	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
456	317	elixp 7915	. . . . . . . . . . . . . . . . . . . . 21 $/\$
457	455, 456	sylibr 224	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
458	457	ex 450	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
459	458	reximdva 3017	. . . . . . . . . . . . . . . . . 18 $/\$
460	375, 459	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$
461		eliun 4524	. . . . . . . . . . . . . . . . 17
462	460, 461	sylibr 224	. . . . . . . . . . . . . . . 16 $/\$
463	462	ralrimiva 2966	. . . . . . . . . . . . . . 15
464		dfss3 3592	. . . . . . . . . . . . . . 15
465	463, 464	sylibr 224	. . . . . . . . . . . . . 14
466		ovexd 6680	. . . . . . . . . . . . . . . . 17
467	228	a1i 11	. . . . . . . . . . . . . . . . 17
468	466, 467	elmapd 7871	. . . . . . . . . . . . . . . 16
469	109, 468	mpbird 247	. . . . . . . . . . . . . . 15
470	466, 467	elmapd 7871	. . . . . . . . . . . . . . . . 17
471	89, 470	mpbird 247	. . . . . . . . . . . . . . . 16
472	82, 71	elmapd 7871	. . . . . . . . . . . . . . . . . 18
473	204, 472	mpbird 247	. . . . . . . . . . . . . . . . 17
474	82, 71	elmapd 7871	. . . . . . . . . . . . . . . . . . 19
475	202, 474	mpbird 247	. . . . . . . . . . . . . . . . . 18
476		hoidmvlelem3.i	. . . . . . . . . . . . . . . . . 18 Σ^{^}
477		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
478	477	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
479	250	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
480	478, 479	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
481	480	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
482	481	ixpeq2dva 7923	. . . . . . . . . . . . . . . . . . . . . . . 24
483	482	sseq1d 3632	. . . . . . . . . . . . . . . . . . . . . . 23
484		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . 24
485	484	breq1d 4663	. . . . . . . . . . . . . . . . . . . . . . 23 Σ^{^} Σ^{^}
486	483, 485	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . 22 Σ^{^} Σ^{^}
487	486	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . 21 Σ^{^} Σ^{^}
488	487	ralbidv 2986	. . . . . . . . . . . . . . . . . . . 20 Σ^{^} Σ^{^}
489	488	ralbidv 2986	. . . . . . . . . . . . . . . . . . 19 Σ^{^} Σ^{^}
490	489	rspcva 3307	. . . . . . . . . . . . . . . . . 18 $/\$ Σ^{^} Σ^{^}
491	475, 476, 490	syl2anc 693	. . . . . . . . . . . . . . . . 17 Σ^{^}
492		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . . . 26
493	492	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
494	251	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
495	493, 494	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
496	495	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
497	496	ixpeq2dva 7923	. . . . . . . . . . . . . . . . . . . . . 22
498	497	sseq1d 3632	. . . . . . . . . . . . . . . . . . . . 21
499		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . 22
500	499	breq1d 4663	. . . . . . . . . . . . . . . . . . . . 21 Σ^{^} Σ^{^}
501	498, 500	imbi12d 334	. . . . . . . . . . . . . . . . . . . 20 Σ^{^} Σ^{^}
502	501	ralbidv 2986	. . . . . . . . . . . . . . . . . . 19 Σ^{^} Σ^{^}
503	502	ralbidv 2986	. . . . . . . . . . . . . . . . . 18 Σ^{^} Σ^{^}
504	503	rspcva 3307	. . . . . . . . . . . . . . . . 17 $/\$ Σ^{^} Σ^{^}
505	473, 491, 504	syl2anc 693	. . . . . . . . . . . . . . . 16 Σ^{^}
506		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . . . 24
507	506	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . . 23
508	507	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . 22
509	508	ixpeq2dv 7924	. . . . . . . . . . . . . . . . . . . . 21
510	509	iuneq2d 4547	. . . . . . . . . . . . . . . . . . . 20
511	510	sseq2d 3633	. . . . . . . . . . . . . . . . . . 19
512	506	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . 22
513	512	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . . . 21
514	513	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 Σ^{^} Σ^{^}
515	514	breq2d 4665	. . . . . . . . . . . . . . . . . . 19 Σ^{^} Σ^{^}
516	511, 515	imbi12d 334	. . . . . . . . . . . . . . . . . 18 Σ^{^} Σ^{^}
517	516	ralbidv 2986	. . . . . . . . . . . . . . . . 17 Σ^{^} Σ^{^}
518	517	rspcva 3307	. . . . . . . . . . . . . . . 16 $/\$ Σ^{^} Σ^{^}
519	471, 505, 518	syl2anc 693	. . . . . . . . . . . . . . 15 Σ^{^}
520		fveq1 6190	. . . . . . . . . . . . . . . . . . . . . 22
521	520	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . 21
522	521	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20
523	522	ixpeq2dv 7924	. . . . . . . . . . . . . . . . . . 19
524	523	iuneq2d 4547	. . . . . . . . . . . . . . . . . 18
525	524	sseq2d 3633	. . . . . . . . . . . . . . . . 17
526	520	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20
527	526	mpteq2dv 4745	. . . . . . . . . . . . . . . . . . 19
528	527	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 Σ^{^} Σ^{^}
529	528	breq2d 4665	. . . . . . . . . . . . . . . . 17 Σ^{^} Σ^{^}
530	525, 529	imbi12d 334	. . . . . . . . . . . . . . . 16 Σ^{^} Σ^{^}
531	530	rspcva 3307	. . . . . . . . . . . . . . 15 $/\$ Σ^{^} Σ^{^}
532	469, 519, 531	syl2anc 693	. . . . . . . . . . . . . 14 Σ^{^}
533	465, 532	mpd 15	. . . . . . . . . . . . 13 Σ^{^}
534		idd 24	. . . . . . . . . . . . 13 Σ^{^} Σ^{^}
535	533, 534	mpd 15	. . . . . . . . . . . 12 Σ^{^}
536	535	adantr 481	. . . . . . . . . . 11 $/\$ Σ^{^}
537	41	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$
538	537	mpteq2dva 4744	. . . . . . . . . . . . 13 $/\$
539	538	fveq2d 6195	. . . . . . . . . . . 12 $/\$ Σ^{^} Σ^{^}
540	249, 539	breq12d 4666	. . . . . . . . . . 11 $/\$ Σ^{^} Σ^{^}
541	536, 540	mpbird 247	. . . . . . . . . 10 $/\$ Σ^{^}
542	541	adantr 481	. . . . . . . . 9 $/\$ $/\$ Σ^{^} Σ^{^}
543	238, 240, 241, 281, 542	ltletrd 10197	. . . . . . . 8 $/\$ $/\$ Σ^{^} Σ^{^}
544	226, 237, 543	syl2anc 693	. . . . . . 7 $/\$ $/\$ Σ^{^} Σ^{^}
545	225, 544	pm2.61dan 832	. . . . . 6 $/\$ Σ^{^}
546	196, 197, 198, 199, 218, 545	sge0uzfsumgt 40661	. . . . 5 $/\$
547	217	adantr 481	. . . . . . . . . . 11 $/\$
548		fzfid 12772	. . . . . . . . . . . . 13
549		simpl 473	. . . . . . . . . . . . . 14 $/\$
550		elfznn 12370	. . . . . . . . . . . . . . 15
551	550	adantl 482	. . . . . . . . . . . . . 14 $/\$
552	28, 114	sseldi 3601	. . . . . . . . . . . . . 14 $/\$
553	549, 551, 552	syl2anc 693	. . . . . . . . . . . . 13 $/\$
554	548, 553	fsumrecl 14465	. . . . . . . . . . . 12
555	554	adantr 481	. . . . . . . . . . 11 $/\$
556		simpr 477	. . . . . . . . . . 11 $/\$
557	547, 555, 556	ltled 10185	. . . . . . . . . 10 $/\$
558	207	adantr 481	. . . . . . . . . . 11 $/\$
559	213	adantr 481	. . . . . . . . . . 11 $/\$
560	558, 555, 559	ledivmuld 11925	. . . . . . . . . 10 $/\$
561	557, 560	mpbid 222	. . . . . . . . 9 $/\$
562	561	ex 450	. . . . . . . 8
563	562	adantr 481	. . . . . . 7 $/\$
564	563	adantlr 751	. . . . . 6 $/\$ $/\$
565	564	reximdva 3017	. . . . 5 $/\$
566	546, 565	mpd 15	. . . 4 $/\$
567	193, 195, 566	syl2anc 693	. . 3 $/\$
568	192, 567	pm2.61dan 832	. 2
569	43	3ad2ant1 1082	. . . . 5 $/\$ $/\$
570	46	3ad2ant1 1082	. . . . 5 $/\$ $/\$
571	47	3ad2ant1 1082	. . . . 5 $/\$ $/\$ $\$
572	200	3ad2ant1 1082	. . . . 5 $/\$ $/\$
573	203	3ad2ant1 1082	. . . . 5 $/\$ $/\$
574	62	3ad2ant1 1082	. . . . 5 $/\$ $/\$
575		eqid 2622	. . . . 5
576		eqid 2622	. . . . 5
577	95	3ad2ant1 1082	. . . . 5 $/\$ $/\$
578		eqid 2622	. . . . 5
579		fveq2 6191	. . . . . . . . . 10
580		fveq2 6191	. . . . . . . . . 10
581	579, 580	oveq12d 6668	. . . . . . . . 9
582	581	cbvmptv 4750	. . . . . . . 8
583	582	fveq2i 6194	. . . . . . 7 Σ^{^} Σ^{^}
584		hoidmvlelem3.r	. . . . . . 7 Σ^{^}
585	583, 584	syl5eqel 2705	. . . . . 6 Σ^{^}
586	585	3ad2ant1 1082	. . . . 5 $/\$ $/\$ Σ^{^}
587		hoidmvlelem3.h	. . . . . 6
588		eleq1 2689	. . . . . . . . . 10
589		fveq2 6191	. . . . . . . . . 10
590	589	breq1d 4663	. . . . . . . . . . 11
591	590, 589	ifbieq1d 4109	. . . . . . . . . 10
592	588, 589, 591	ifbieq12d 4113	. . . . . . . . 9
593	592	cbvmptv 4750	. . . . . . . 8
594	593	mpteq2i 4741	. . . . . . 7
595	594	mpteq2i 4741	. . . . . 6
596	587, 595	eqtri 2644	. . . . 5
597	172	3ad2ant1 1082	. . . . 5 $/\$ $/\$
598		fveq2 6191	. . . . . . . . . . . . 13
599		fveq2 6191	. . . . . . . . . . . . . 14
600	599	fveq2d 6195	. . . . . . . . . . . . 13
601	598, 600	oveq12d 6668	. . . . . . . . . . . 12
602	601	cbvmptv 4750	. . . . . . . . . . 11
603	602	fveq2i 6194	. . . . . . . . . 10 Σ^{^} Σ^{^}
604	603	oveq2i 6661	. . . . . . . . 9 Σ^{^} Σ^{^}
605	604	breq2i 4661	. . . . . . . 8 Σ^{^} Σ^{^}
606	605	a1i 11	. . . . . . 7 Σ^{^} Σ^{^}
607	606	rabbiia 3185	. . . . . 6 Σ^{^} Σ^{^}
608	337, 607	eqtri 2644	. . . . 5 Σ^{^}
609	285	3ad2ant1 1082	. . . . 5 $/\$ $/\$
610	344	3ad2ant1 1082	. . . . 5 $/\$ $/\$
611		eqid 2622	. . . . 5
612		simp2 1062	. . . . 5 $/\$ $/\$
613		id 22	. . . . . . . 8
614		fveq2 6191	. . . . . . . . . . 11
615	614	cbvsumv 14426	. . . . . . . . . 10
616	615	oveq2i 6661	. . . . . . . . 9
617	616	a1i 11	. . . . . . . 8
618	613, 617	breqtrd 4679	. . . . . . 7
619	618	3ad2ant3 1084	. . . . . 6 $/\$ $/\$
620		simpl 473	. . . . . . . . . 10 $/\$
621		elfznn 12370	. . . . . . . . . . 11
622	621	adantl 482	. . . . . . . . . 10 $/\$
623		eleq1 2689	. . . . . . . . . . . . . . 15
624		fveq2 6191	. . . . . . . . . . . . . . . . 17
625		fveq2 6191	. . . . . . . . . . . . . . . . 17
626	624, 625	oveq12d 6668	. . . . . . . . . . . . . . . 16
627	614, 626	eqeq12d 2637	. . . . . . . . . . . . . . 15
628	623, 627	imbi12d 334	. . . . . . . . . . . . . 14
629	628, 41	chvarv 2263	. . . . . . . . . . . . 13
630	629	adantl 482	. . . . . . . . . . . 12 $/\$
631	623	anbi2d 740	. . . . . . . . . . . . . . 15 $/\$ $/\$
632	598	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19
633	599	fveq1d 6193	. . . . . . . . . . . . . . . . . . 19
634	632, 633	oveq12d 6668	. . . . . . . . . . . . . . . . . 18
635	634	eleq2d 2687	. . . . . . . . . . . . . . . . 17
636	598	reseq1d 5395	. . . . . . . . . . . . . . . . 17
637	635, 636	ifbieq1d 4109	. . . . . . . . . . . . . . . 16
638	624, 637	eqeq12d 2637	. . . . . . . . . . . . . . 15
639	631, 638	imbi12d 334	. . . . . . . . . . . . . 14 $/\$ $/\$
640	639, 149	chvarv 2263	. . . . . . . . . . . . 13 $/\$
641	599	reseq1d 5395	. . . . . . . . . . . . . . . . 17
642	635, 641	ifbieq1d 4109	. . . . . . . . . . . . . . . 16
643	625, 642	eqeq12d 2637	. . . . . . . . . . . . . . 15
644	631, 643	imbi12d 334	. . . . . . . . . . . . . 14 $/\$ $/\$
645	644, 440	chvarv 2263	. . . . . . . . . . . . 13 $/\$
646	640, 645	oveq12d 6668	. . . . . . . . . . . 12 $/\$
647	630, 646	eqtrd 2656	. . . . . . . . . . 11 $/\$
648		simpr 477	. . . . . . . . . . . . 13 $/\$
649		ovexd 6680	. . . . . . . . . . . . 13 $/\$
650	611	fvmpt2 6291	. . . . . . . . . . . . 13 $/\$
651	648, 649, 650	syl2anc 693	. . . . . . . . . . . 12 $/\$
652		fvex 6201	. . . . . . . . . . . . . . . . . . 19
653	652	resex 5443	. . . . . . . . . . . . . . . . . 18
654	653	a1i 11	. . . . . . . . . . . . . . . . 17
655	80, 143	syl5eqelr 2706	. . . . . . . . . . . . . . . . 17
656	654, 655	ifcld 4131	. . . . . . . . . . . . . . . 16
657	656	adantr 481	. . . . . . . . . . . . . . 15 $/\$
658	576	fvmpt2 6291	. . . . . . . . . . . . . . 15 $/\$
659	648, 657, 658	syl2anc 693	. . . . . . . . . . . . . 14 $/\$
660	80	eqcomi 2631	. . . . . . . . . . . . . . . 16
661		ifeq2 4091	. . . . . . . . . . . . . . . 16
662	660, 661	ax-mp 5	. . . . . . . . . . . . . . 15
663	662	a1i 11	. . . . . . . . . . . . . 14 $/\$
664	659, 663	eqtrd 2656	. . . . . . . . . . . . 13 $/\$
665		fvex 6201	. . . . . . . . . . . . . . . . . . 19
666	665	resex 5443	. . . . . . . . . . . . . . . . . 18
667	666	a1i 11	. . . . . . . . . . . . . . . . 17
668	667, 655	ifcld 4131	. . . . . . . . . . . . . . . 16
669	668	adantr 481	. . . . . . . . . . . . . . 15 $/\$
670	578	fvmpt2 6291	. . . . . . . . . . . . . . 15 $/\$
671	648, 669, 670	syl2anc 693	. . . . . . . . . . . . . 14 $/\$
672		biid 251	. . . . . . . . . . . . . . . 16
673	672, 660	ifbieq2i 4110	. . . . . . . . . . . . . . 15
674	673	a1i 11	. . . . . . . . . . . . . 14 $/\$
675	671, 674	eqtrd 2656	. . . . . . . . . . . . 13 $/\$
676	664, 675	oveq12d 6668	. . . . . . . . . . . 12 $/\$
677	651, 676	eqtrd 2656	. . . . . . . . . . 11 $/\$
678	647, 677	eqtr4d 2659	. . . . . . . . . 10 $/\$
679	620, 622, 678	syl2anc 693	. . . . . . . . 9 $/\$
680	679	3ad2antl1 1223	. . . . . . . 8 $/\$ $/\$ $/\$
681	680	sumeq2dv 14433	. . . . . . 7 $/\$ $/\$
682	681	oveq2d 6666	. . . . . 6 $/\$ $/\$
683	619, 682	breqtrd 4679	. . . . 5 $/\$ $/\$
684		fveq2 6191	. . . . . . . 8
685	684	fveq1d 6193	. . . . . . 7
686	685	cbvmptv 4750	. . . . . 6
687	686	rneqi 5352	. . . . 5
688		fveq2 6191	. . . . . . . . . . . 12
689	688	fveq1d 6193	. . . . . . . . . . 11
690		fveq2 6191	. . . . . . . . . . . 12
691	690	fveq1d 6193	. . . . . . . . . . 11
692	689, 691	oveq12d 6668	. . . . . . . . . 10
693	692	eleq2d 2687	. . . . . . . . 9
694	693	cbvrabv 3199	. . . . . . . 8
695	694	mpteq1i 4739	. . . . . . 7
696	695	rneqi 5352	. . . . . 6
697	696	uneq2i 3764	. . . . 5
698		eqid 2622	. . . . 5 inf inf
699	18, 569, 570, 571, 44, 572, 573, 574, 575, 576, 577, 578, 586, 596, 5, 597, 608, 609, 610, 611, 612, 683, 687, 697, 698	hoidmvlelem2 40810	. . . 4 $/\$ $/\$
700	699	3exp 1264	. . 3
701	700	rexlimdv 3030	. 2
702	568, 701	mpd 15	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200 $\$ cdif 3571

cun 3572

wss 3574

c0 3915

cif 4086

csn 4177

ciun 4520 class class class wbr 4653

cmpt 4729

crn 5115

cres 5116

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cmpt2 6652

cmap 7857

cixp 7908

cfn 7955 infcinf 8347

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cpnf 10071

cxr 10073

clt 10074

cle 10075

cmin 10266

cdiv 10684

cn 11020

cz 11377

crp 11832

cico 12177

cicc 12178

cfz 12326

csu 14416

cprod 14635

cvol 23232 Σ^{^}csumge0 40579

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-ixp 7909 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-rlim 14220 df-sum 14417 df-prod 14636 df-rest 16083 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750 df-cmp 21190 df-ovol 23233 df-vol 23234 df-sumge0 40580

This theorem is referenced by: hoidmvlelem4 40812

W3C validator