mblfinlem4 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mblfinlem4		Structured version Unicode version

Theorem mblfinlem4 30029

Description: Backward direction of ismblfin 30030. (Contributed by Brendan Leahy, 28-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)

**Assertion**
Ref	Expression
mblfinlem4	$/\$ $/\$ $/\$

Distinct variable group:

Proof of Theorem mblfinlem4 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltso 9668	. . . 4
2	1	a1i 11	. . 3 $/\$ $/\$
3		simplr 755	. . 3 $/\$ $/\$
4		vex 3098	. . . . . . 7
5		eqeq1 2447	. . . . . . . . 9
6	5	anbi2d 703	. . . . . . . 8 $/\$ $/\$
7	6	rexbidv 2954	. . . . . . 7 $/\$ $/\$
8	4, 7	elab 3232	. . . . . 6 $/\$ $/\$
9		simprl 756	. . . . . . . . 9 $/\$ $/\$
10		ovolss 21769	. . . . . . . . . . 11 $/\$
11		sstr 3497	. . . . . . . . . . . . 13 $/\$
12		ovolcl 21762	. . . . . . . . . . . . 13
13	11, 12	syl 16	. . . . . . . . . . . 12 $/\$
14		ovolcl 21762	. . . . . . . . . . . . 13
15	14	adantl 466	. . . . . . . . . . . 12 $/\$
16		xrlenlt 9655	. . . . . . . . . . . 12 $/\$
17	13, 15, 16	syl2anc 661	. . . . . . . . . . 11 $/\$
18	10, 17	mpbid 210	. . . . . . . . . 10 $/\$
19	18	ancoms 453	. . . . . . . . 9 $/\$
20	9, 19	sylan2 474	. . . . . . . 8 $/\$ $/\$ $/\$
21		simprrr 766	. . . . . . . . . 10 $/\$ $/\$ $/\$
22		uniretop 21142	. . . . . . . . . . . . . . 15
23	22	cldss 19403	. . . . . . . . . . . . . 14
24		dfss4 3717	. . . . . . . . . . . . . 14 $\$ $\$
25	23, 24	sylib 196	. . . . . . . . . . . . 13 $\$ $\$
26		rembl 21824	. . . . . . . . . . . . . 14
27	22	cldopn 19405	. . . . . . . . . . . . . . 15 $\$
28		opnmbl 21884	. . . . . . . . . . . . . . 15 $\$ $\$
29	27, 28	syl 16	. . . . . . . . . . . . . 14 $\$
30		difmbl 21826	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$
31	26, 29, 30	sylancr 663	. . . . . . . . . . . . 13 $\$ $\$
32	25, 31	eqeltrrd 2532	. . . . . . . . . . . 12
33		mblvol 21814	. . . . . . . . . . . 12
34	32, 33	syl 16	. . . . . . . . . . 11
35	34	ad2antrl 727	. . . . . . . . . 10 $/\$ $/\$ $/\$
36	21, 35	eqtrd 2484	. . . . . . . . 9 $/\$ $/\$ $/\$
37	36	breq2d 4449	. . . . . . . 8 $/\$ $/\$ $/\$
38	20, 37	mtbird 301	. . . . . . 7 $/\$ $/\$ $/\$
39	38	rexlimdvaa 2936	. . . . . 6 $/\$
40	8, 39	syl5bi 217	. . . . 5 $/\$
41	40	ad2antrr 725	. . . 4 $/\$ $/\$ $/\$
42	41	imp 429	. . 3 $/\$ $/\$ $/\$ $/\$
43		1rp 11233	. . . . . . . . 9
44		eqid 2443	. . . . . . . . . 10
45	44	ovolgelb 21764	. . . . . . . . 9 $/\$ $/\$ $/\$
46	43, 45	mp3an3 1314	. . . . . . . 8 $/\$ $/\$
47		elmapi 7442	. . . . . . . . . . 11
48		ssid 3508	. . . . . . . . . . . . . . 15
49	44	ovollb 21763	. . . . . . . . . . . . . . 15 $/\$
50	48, 49	mpan2 671	. . . . . . . . . . . . . 14
51	50	adantl 466	. . . . . . . . . . . . 13 $/\$
52		eqid 2443	. . . . . . . . . . . . . . . 16
53	52, 44	ovolsf 21757	. . . . . . . . . . . . . . 15
54		frn 5727	. . . . . . . . . . . . . . . 16
55		icossxr 11618	. . . . . . . . . . . . . . . 16
56	54, 55	syl6ss 3501	. . . . . . . . . . . . . . 15
57		supxrcl 11515	. . . . . . . . . . . . . . 15
58	53, 56, 57	3syl 20	. . . . . . . . . . . . . 14
59		peano2re 9756	. . . . . . . . . . . . . . 15
60	59	rexrd 9646	. . . . . . . . . . . . . 14
61		rncoss 5253	. . . . . . . . . . . . . . . . . 18
62	61	unissi 4257	. . . . . . . . . . . . . . . . 17
63		unirnioo 11633	. . . . . . . . . . . . . . . . 17
64	62, 63	sseqtr4i 3522	. . . . . . . . . . . . . . . 16
65		ovolcl 21762	. . . . . . . . . . . . . . . 16
66	64, 65	ax-mp 5	. . . . . . . . . . . . . . 15
67		xrletr 11370	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
68	66, 67	mp3an1 1312	. . . . . . . . . . . . . 14 $/\$ $/\$
69	58, 60, 68	syl2anr 478	. . . . . . . . . . . . 13 $/\$ $/\$
70	51, 69	mpand 675	. . . . . . . . . . . 12 $/\$
71	70	adantll 713	. . . . . . . . . . 11 $/\$ $/\$
72	47, 71	sylan2 474	. . . . . . . . . 10 $/\$ $/\$
73	72	anim2d 565	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74	73	reximdva 2918	. . . . . . . 8 $/\$ $/\$ $/\$
75	46, 74	mpd 15	. . . . . . 7 $/\$ $/\$
76		rexex 2900	. . . . . . 7 $/\$ $/\$
77	75, 76	syl 16	. . . . . 6 $/\$ $/\$
78	77	ad2antrr 725	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
79		difss 3616	. . . . . . . . . . . . . 14 $\$
80	79, 64	sstri 3498	. . . . . . . . . . . . 13 $\$
81		ovolcl 21762	. . . . . . . . . . . . 13 $\$ $\$
82	80, 81	ax-mp 5	. . . . . . . . . . . 12 $\$
83	59, 82	jctil 537	. . . . . . . . . . 11 $\$ $/\$
84	83	ad4antlr 732	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
85		ovolss 21769	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
86	79, 64, 85	mp2an 672	. . . . . . . . . . . . . 14 $\$
87		xrletr 11370	. . . . . . . . . . . . . . . 16 $\$ $/\$ $/\$ $\$ $/\$ $\$
88	82, 66, 87	mp3an12 1315	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
89	60, 88	syl 16	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
90	86, 89	mpani 676	. . . . . . . . . . . . 13 $\$
91	90	ad4antlr 732	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
92	91	impr 619	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
93		ovolge0 21765	. . . . . . . . . . . 12 $\$ $\$
94	80, 93	ax-mp 5	. . . . . . . . . . 11 $\$
95	92, 94	jctil 537	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
96		xrrege0 11384	. . . . . . . . . 10 $\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
97	84, 95, 96	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
98		resubcl 9888	. . . . . . . . . . . . . 14 $/\$
99	98	adantrr 716	. . . . . . . . . . . . 13 $/\$ $/\$
100		posdif 10051	. . . . . . . . . . . . . . . 16 $/\$
101	100	ancoms 453	. . . . . . . . . . . . . . 15 $/\$
102	101	biimpd 207	. . . . . . . . . . . . . 14 $/\$
103	102	impr 619	. . . . . . . . . . . . 13 $/\$ $/\$
104	99, 103	elrpd 11263	. . . . . . . . . . . 12 $/\$ $/\$
105	104	rphalfcld 11277	. . . . . . . . . . 11 $/\$ $/\$
106	3, 105	sylan 471	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
107	106	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		eqid 2443	. . . . . . . . . . 11
109	108	ovolgelb 21764	. . . . . . . . . 10 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
110	80, 109	mp3an1 1312	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$
111	97, 107, 110	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
112		elmapi 7442	. . . . . . . . . . 11
113		ssid 3508	. . . . . . . . . . . . . 14
114	108	ovollb 21763	. . . . . . . . . . . . . 14 $/\$
115	113, 114	mpan2 671	. . . . . . . . . . . . 13
116	115	adantl 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
117		eqid 2443	. . . . . . . . . . . . . . 15
118	117, 108	ovolsf 21757	. . . . . . . . . . . . . 14
119		frn 5727	. . . . . . . . . . . . . . 15
120	119, 55	syl6ss 3501	. . . . . . . . . . . . . 14
121		supxrcl 11515	. . . . . . . . . . . . . 14
122	118, 120, 121	3syl 20	. . . . . . . . . . . . 13
123	99	rehalfcld 10791	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
124	3, 123	sylan 471	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
125	124	adantr 465	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	97, 125	readdcld 9626	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
127	126	rexrd 9646	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
128		rncoss 5253	. . . . . . . . . . . . . . . . 17
129	128	unissi 4257	. . . . . . . . . . . . . . . 16
130	129, 63	sseqtr4i 3522	. . . . . . . . . . . . . . 15
131		ovolcl 21762	. . . . . . . . . . . . . . 15
132	130, 131	ax-mp 5	. . . . . . . . . . . . . 14
133		xrletr 11370	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $\$ $\$
134	132, 133	mp3an1 1312	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$
135	122, 127, 134	syl2anr 478	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
136	116, 135	mpand 675	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
137	112, 136	sylan2 474	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
138	137	anim2d 565	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
139	138	reximdva 2918	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
140	111, 139	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
141		rexex 2900	. . . . . . 7 $\$ $/\$ $\$ $\$ $/\$ $\$
142	140, 141	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
143	59, 66	jctil 537	. . . . . . . . . . . 12 $/\$
144	143	ad3antlr 730	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
145		ovolge0 21765	. . . . . . . . . . . . . 14
146	64, 145	ax-mp 5	. . . . . . . . . . . . 13
147	146	jctl 541	. . . . . . . . . . . 12 $/\$
148	147	adantl 466	. . . . . . . . . . 11 $/\$ $/\$
149		xrrege0 11384	. . . . . . . . . . 11 $/\$ $/\$ $/\$
150	144, 148, 149	syl2an 477	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
151	150, 125	resubcld 9993	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
152	150, 107	ltsubrpd 11293	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
153		retop 21141	. . . . . . . . . . 11
154		retopbas 21140	. . . . . . . . . . . . 13
155		bastg 19340	. . . . . . . . . . . . 13
156	154, 155	ax-mp 5	. . . . . . . . . . . 12
157	61, 156	sstri 3498	. . . . . . . . . . 11
158		uniopn 19279	. . . . . . . . . . 11 $/\$
159	153, 157, 158	mp2an 672	. . . . . . . . . 10
160		mblfinlem2 30027	. . . . . . . . . 10 $/\$ $/\$ $/\$
161	159, 160	mp3an1 1312	. . . . . . . . 9 $/\$ $/\$
162	151, 152, 161	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	162	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
164		indif2 3726	. . . . . . . . . . . . . . 15 $\$ $\$
165	22	cldss 19403	. . . . . . . . . . . . . . . . 17
166		df-ss 3475	. . . . . . . . . . . . . . . . 17
167	165, 166	sylib 196	. . . . . . . . . . . . . . . 16
168	167	difeq1d 3606	. . . . . . . . . . . . . . 15 $\$ $\$
169	164, 168	syl5eq 2496	. . . . . . . . . . . . . 14 $\$ $\$
170	128, 156	sstri 3498	. . . . . . . . . . . . . . . . 17
171		uniopn 19279	. . . . . . . . . . . . . . . . 17 $/\$
172	153, 170, 171	mp2an 672	. . . . . . . . . . . . . . . 16
173	22	opncld 19407	. . . . . . . . . . . . . . . 16 $/\$ $\$
174	153, 172, 173	mp2an 672	. . . . . . . . . . . . . . 15 $\$
175		incld 19417	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
176	174, 175	mpan2 671	. . . . . . . . . . . . . 14 $\$
177	169, 176	eqeltrrd 2532	. . . . . . . . . . . . 13 $\$
178		simpr 461	. . . . . . . . . . . . . . 15 $\$ $/\$
179		simpl 457	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
180	178, 179	ssdif2d 3628	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
181		dfin4 3723	. . . . . . . . . . . . . . 15 $\$ $\$
182		inss2 3704	. . . . . . . . . . . . . . 15
183	181, 182	eqsstr3i 3520	. . . . . . . . . . . . . 14 $\$ $\$
184	180, 183	syl6ss 3501	. . . . . . . . . . . . 13 $\$ $/\$ $\$
185		sseq1 3510	. . . . . . . . . . . . . . . 16 $\$ $\$
186	185	anbi1d 704	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $\$ $/\$ $\$
187		fveq2 5856	. . . . . . . . . . . . . . . . 17 $\$ $\$
188	187	eqcoms 2455	. . . . . . . . . . . . . . . 16 $\$ $\$
189	188	biantrud 507	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $/\$ $\$
190	186, 189	bitr4d 256	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$
191	190	rspcev 3196	. . . . . . . . . . . . 13 $\$ $/\$ $\$ $/\$ $\$
192	177, 184, 191	syl2an 477	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $/\$ $\$
193	192	an12s 801	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$
194	193	adantrrr 724	. . . . . . . . . 10 $\$ $/\$ $/\$ $/\$ $/\$ $\$
195	194	adantlr 714	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
196	195	adantll 713	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
197		difss 3616	. . . . . . . . . . . 12 $\$ $\$
198		ovolsscl 21770	. . . . . . . . . . . 12 $\$ $\$ $/\$ $/\$ $\$ $\$
199	197, 198	mp3an1 1312	. . . . . . . . . . 11 $/\$ $\$ $\$
200	199	ad5antr 733	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
201		simp-6r 772	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
202		simpl 457	. . . . . . . . . . 11 $/\$
203	202	ad4antlr 732	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
204		difdif2 3740	. . . . . . . . . . . 12 $\$ $\$ $\$
205	204	fveq2i 5859	. . . . . . . . . . 11 $\$ $\$ $\$
206		difss 3616	. . . . . . . . . . . . . . 15 $\$
207		inss1 3703	. . . . . . . . . . . . . . 15
208	206, 207	unssi 3664	. . . . . . . . . . . . . 14 $\$
209		ovolsscl 21770	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$
210	208, 209	mp3an1 1312	. . . . . . . . . . . . 13 $/\$ $\$
211	210	ad5antr 733	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
212		ovolsscl 21770	. . . . . . . . . . . . . . 15 $\$ $/\$ $/\$ $\$
213	206, 212	mp3an1 1312	. . . . . . . . . . . . . 14 $/\$ $\$
214	213	ad5antr 733	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
215		ovolsscl 21770	. . . . . . . . . . . . . . 15 $/\$ $/\$
216	207, 215	mp3an1 1312	. . . . . . . . . . . . . 14 $/\$
217	216	ad5antr 733	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
218	214, 217	readdcld 9626	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
219	3, 202, 98	syl2an 477	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
220	219	ad3antrrr 729	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
221		ssdifss 3620	. . . . . . . . . . . . . . 15 $\$
222	221	adantr 465	. . . . . . . . . . . . . 14 $/\$ $\$
223		ssinss1 3711	. . . . . . . . . . . . . . 15
224	223	adantr 465	. . . . . . . . . . . . . 14 $/\$
225		ovolun 21783	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
226	222, 213, 224, 216, 225	syl22anc 1230	. . . . . . . . . . . . 13 $/\$ $\$ $\$
227	226	ad5antr 733	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
228	124	ad2antrr 725	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
229	228	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
230	150	ad2antrr 725	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
231		simprl 756	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
232	150	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
233		ovolsscl 21770	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
234	64, 233	mp3an2 1313	. . . . . . . . . . . . . . . . 17 $/\$
235	231, 232, 234	syl2anr 478	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$