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 30294

Description: Backward direction of ismblfin 30295. (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 9654	. . . 4
2	1	a1i 11	. . 3 $/\$ $/\$
3		simplr 753	. . 3 $/\$ $/\$
4		vex 3109	. . . . . . 7
5		eqeq1 2458	. . . . . . . . 9
6	5	anbi2d 701	. . . . . . . 8 $/\$ $/\$
7	6	rexbidv 2965	. . . . . . 7 $/\$ $/\$
8	4, 7	elab 3243	. . . . . 6 $/\$ $/\$
9		simprl 754	. . . . . . . . 9 $/\$ $/\$
10		ovolss 22062	. . . . . . . . . . 11 $/\$
11		sstr 3497	. . . . . . . . . . . . 13 $/\$
12		ovolcl 22055	. . . . . . . . . . . . 13
13	11, 12	syl 16	. . . . . . . . . . . 12 $/\$
14		ovolcl 22055	. . . . . . . . . . . . 13
15	14	adantl 464	. . . . . . . . . . . 12 $/\$
16		xrlenlt 9641	. . . . . . . . . . . 12 $/\$
17	13, 15, 16	syl2anc 659	. . . . . . . . . . 11 $/\$
18	10, 17	mpbid 210	. . . . . . . . . 10 $/\$
19	18	ancoms 451	. . . . . . . . 9 $/\$
20	9, 19	sylan2 472	. . . . . . . 8 $/\$ $/\$ $/\$
21		simprrr 764	. . . . . . . . . 10 $/\$ $/\$ $/\$
22		uniretop 21435	. . . . . . . . . . . . . . 15
23	22	cldss 19697	. . . . . . . . . . . . . 14
24		dfss4 3729	. . . . . . . . . . . . . 14 $\$ $\$
25	23, 24	sylib 196	. . . . . . . . . . . . 13 $\$ $\$
26		rembl 22117	. . . . . . . . . . . . . 14
27	22	cldopn 19699	. . . . . . . . . . . . . . 15 $\$
28		opnmbl 22177	. . . . . . . . . . . . . . 15 $\$ $\$
29	27, 28	syl 16	. . . . . . . . . . . . . 14 $\$
30		difmbl 22119	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$
31	26, 29, 30	sylancr 661	. . . . . . . . . . . . 13 $\$ $\$
32	25, 31	eqeltrrd 2543	. . . . . . . . . . . 12
33		mblvol 22107	. . . . . . . . . . . 12
34	32, 33	syl 16	. . . . . . . . . . 11
35	34	ad2antrl 725	. . . . . . . . . 10 $/\$ $/\$ $/\$
36	21, 35	eqtrd 2495	. . . . . . . . 9 $/\$ $/\$ $/\$
37	36	breq2d 4451	. . . . . . . 8 $/\$ $/\$ $/\$
38	20, 37	mtbird 299	. . . . . . 7 $/\$ $/\$ $/\$
39	38	rexlimdvaa 2947	. . . . . 6 $/\$
40	8, 39	syl5bi 217	. . . . 5 $/\$
41	40	ad2antrr 723	. . . 4 $/\$ $/\$ $/\$
42	41	imp 427	. . 3 $/\$ $/\$ $/\$ $/\$
43		1rp 11225	. . . . . . . . 9
44		eqid 2454	. . . . . . . . . 10
45	44	ovolgelb 22057	. . . . . . . . 9 $/\$ $/\$ $/\$
46	43, 45	mp3an3 1311	. . . . . . . 8 $/\$ $/\$
47		elmapi 7433	. . . . . . . . . . 11
48		ssid 3508	. . . . . . . . . . . . . . 15
49	44	ovollb 22056	. . . . . . . . . . . . . . 15 $/\$
50	48, 49	mpan2 669	. . . . . . . . . . . . . 14
51	50	adantl 464	. . . . . . . . . . . . 13 $/\$
52		eqid 2454	. . . . . . . . . . . . . . . 16
53	52, 44	ovolsf 22050	. . . . . . . . . . . . . . 15
54		frn 5719	. . . . . . . . . . . . . . . 16
55		icossxr 11612	. . . . . . . . . . . . . . . 16
56	54, 55	syl6ss 3501	. . . . . . . . . . . . . . 15
57		supxrcl 11509	. . . . . . . . . . . . . . 15
58	53, 56, 57	3syl 20	. . . . . . . . . . . . . 14
59		peano2re 9742	. . . . . . . . . . . . . . 15
60	59	rexrd 9632	. . . . . . . . . . . . . 14
61		rncoss 5252	. . . . . . . . . . . . . . . . . 18
62	61	unissi 4258	. . . . . . . . . . . . . . . . 17
63		unirnioo 11627	. . . . . . . . . . . . . . . . 17
64	62, 63	sseqtr4i 3522	. . . . . . . . . . . . . . . 16
65		ovolcl 22055	. . . . . . . . . . . . . . . 16
66	64, 65	ax-mp 5	. . . . . . . . . . . . . . 15
67		xrletr 11364	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
68	66, 67	mp3an1 1309	. . . . . . . . . . . . . 14 $/\$ $/\$
69	58, 60, 68	syl2anr 476	. . . . . . . . . . . . 13 $/\$ $/\$
70	51, 69	mpand 673	. . . . . . . . . . . 12 $/\$
71	70	adantll 711	. . . . . . . . . . 11 $/\$ $/\$
72	47, 71	sylan2 472	. . . . . . . . . 10 $/\$ $/\$
73	72	anim2d 563	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74	73	reximdva 2929	. . . . . . . 8 $/\$ $/\$ $/\$
75	46, 74	mpd 15	. . . . . . 7 $/\$ $/\$
76		rexex 2911	. . . . . . 7 $/\$ $/\$
77	75, 76	syl 16	. . . . . 6 $/\$ $/\$
78	77	ad2antrr 723	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
79		difss 3617	. . . . . . . . . . . . . 14 $\$
80	79, 64	sstri 3498	. . . . . . . . . . . . 13 $\$
81		ovolcl 22055	. . . . . . . . . . . . 13 $\$ $\$
82	80, 81	ax-mp 5	. . . . . . . . . . . 12 $\$
83	59, 82	jctil 535	. . . . . . . . . . 11 $\$ $/\$
84	83	ad4antlr 730	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
85		ovolss 22062	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
86	79, 64, 85	mp2an 670	. . . . . . . . . . . . . 14 $\$
87		xrletr 11364	. . . . . . . . . . . . . . . 16 $\$ $/\$ $/\$ $\$ $/\$ $\$
88	82, 66, 87	mp3an12 1312	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
89	60, 88	syl 16	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
90	86, 89	mpani 674	. . . . . . . . . . . . 13 $\$
91	90	ad4antlr 730	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
92	91	impr 617	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
93		ovolge0 22058	. . . . . . . . . . . 12 $\$ $\$
94	80, 93	ax-mp 5	. . . . . . . . . . 11 $\$
95	92, 94	jctil 535	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
96		xrrege0 11378	. . . . . . . . . 10 $\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
97	84, 95, 96	syl2anc 659	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
98		resubcl 9874	. . . . . . . . . . . . . 14 $/\$
99	98	adantrr 714	. . . . . . . . . . . . 13 $/\$ $/\$
100		posdif 10041	. . . . . . . . . . . . . . . 16 $/\$
101	100	ancoms 451	. . . . . . . . . . . . . . 15 $/\$
102	101	biimpd 207	. . . . . . . . . . . . . 14 $/\$
103	102	impr 617	. . . . . . . . . . . . 13 $/\$ $/\$
104	99, 103	elrpd 11256	. . . . . . . . . . . 12 $/\$ $/\$
105	104	rphalfcld 11271	. . . . . . . . . . 11 $/\$ $/\$
106	3, 105	sylan 469	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
107	106	adantr 463	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		eqid 2454	. . . . . . . . . . 11
109	108	ovolgelb 22057	. . . . . . . . . 10 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
110	80, 109	mp3an1 1309	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$
111	97, 107, 110	syl2anc 659	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
112		elmapi 7433	. . . . . . . . . . 11
113		ssid 3508	. . . . . . . . . . . . . 14
114	108	ovollb 22056	. . . . . . . . . . . . . 14 $/\$
115	113, 114	mpan2 669	. . . . . . . . . . . . 13
116	115	adantl 464	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
117		eqid 2454	. . . . . . . . . . . . . . 15
118	117, 108	ovolsf 22050	. . . . . . . . . . . . . 14
119		frn 5719	. . . . . . . . . . . . . . 15
120	119, 55	syl6ss 3501	. . . . . . . . . . . . . 14
121		supxrcl 11509	. . . . . . . . . . . . . 14
122	118, 120, 121	3syl 20	. . . . . . . . . . . . 13
123	99	rehalfcld 10781	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
124	3, 123	sylan 469	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
125	124	adantr 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	97, 125	readdcld 9612	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
127	126	rexrd 9632	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
128		rncoss 5252	. . . . . . . . . . . . . . . . 17
129	128	unissi 4258	. . . . . . . . . . . . . . . 16
130	129, 63	sseqtr4i 3522	. . . . . . . . . . . . . . 15
131		ovolcl 22055	. . . . . . . . . . . . . . 15
132	130, 131	ax-mp 5	. . . . . . . . . . . . . 14
133		xrletr 11364	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $\$ $\$
134	132, 133	mp3an1 1309	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$
135	122, 127, 134	syl2anr 476	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
136	116, 135	mpand 673	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
137	112, 136	sylan2 472	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
138	137	anim2d 563	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
139	138	reximdva 2929	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
140	111, 139	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
141		rexex 2911	. . . . . . 7 $\$ $/\$ $\$ $\$ $/\$ $\$
142	140, 141	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
143	59, 66	jctil 535	. . . . . . . . . . . 12 $/\$
144	143	ad3antlr 728	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
145		ovolge0 22058	. . . . . . . . . . . . . 14
146	64, 145	ax-mp 5	. . . . . . . . . . . . 13
147	146	jctl 539	. . . . . . . . . . . 12 $/\$
148	147	adantl 464	. . . . . . . . . . 11 $/\$ $/\$
149		xrrege0 11378	. . . . . . . . . . 11 $/\$ $/\$ $/\$
150	144, 148, 149	syl2an 475	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
151	150, 125	resubcld 9983	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
152	150, 107	ltsubrpd 11287	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
153		retop 21434	. . . . . . . . . . 11
154		retopbas 21433	. . . . . . . . . . . . 13
155		bastg 19634	. . . . . . . . . . . . 13
156	154, 155	ax-mp 5	. . . . . . . . . . . 12
157	61, 156	sstri 3498	. . . . . . . . . . 11
158		uniopn 19573	. . . . . . . . . . 11 $/\$
159	153, 157, 158	mp2an 670	. . . . . . . . . 10
160		mblfinlem2 30292	. . . . . . . . . 10 $/\$ $/\$ $/\$
161	159, 160	mp3an1 1309	. . . . . . . . 9 $/\$ $/\$
162	151, 152, 161	syl2anc 659	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	162	adantr 463	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
164		indif2 3738	. . . . . . . . . . . . . . 15 $\$ $\$
165	22	cldss 19697	. . . . . . . . . . . . . . . . 17
166		df-ss 3475	. . . . . . . . . . . . . . . . 17
167	165, 166	sylib 196	. . . . . . . . . . . . . . . 16
168	167	difeq1d 3607	. . . . . . . . . . . . . . 15 $\$ $\$
169	164, 168	syl5eq 2507	. . . . . . . . . . . . . 14 $\$ $\$
170	128, 156	sstri 3498	. . . . . . . . . . . . . . . . 17
171		uniopn 19573	. . . . . . . . . . . . . . . . 17 $/\$
172	153, 170, 171	mp2an 670	. . . . . . . . . . . . . . . 16
173	22	opncld 19701	. . . . . . . . . . . . . . . 16 $/\$ $\$
174	153, 172, 173	mp2an 670	. . . . . . . . . . . . . . 15 $\$
175		incld 19711	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
176	174, 175	mpan2 669	. . . . . . . . . . . . . 14 $\$
177	169, 176	eqeltrrd 2543	. . . . . . . . . . . . 13 $\$
178		simpr 459	. . . . . . . . . . . . . . 15 $\$ $/\$
179		simpl 455	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
180	178, 179	ssdif2d 3629	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
181		dfin4 3735	. . . . . . . . . . . . . . 15 $\$ $\$
182		inss2 3705	. . . . . . . . . . . . . . 15
183	181, 182	eqsstr3i 3520	. . . . . . . . . . . . . 14 $\$ $\$
184	180, 183	syl6ss 3501	. . . . . . . . . . . . 13 $\$ $/\$ $\$
185		sseq1 3510	. . . . . . . . . . . . . . . 16 $\$ $\$
186	185	anbi1d 702	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $\$ $/\$ $\$
187		fveq2 5848	. . . . . . . . . . . . . . . . 17 $\$ $\$
188	187	eqcoms 2466	. . . . . . . . . . . . . . . 16 $\$ $\$
189	188	biantrud 505	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $/\$ $\$
190	186, 189	bitr4d 256	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$
191	190	rspcev 3207	. . . . . . . . . . . . 13 $\$ $/\$ $\$ $/\$ $\$
192	177, 184, 191	syl2an 475	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $/\$ $\$
193	192	an12s 799	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$
194	193	adantrrr 722	. . . . . . . . . 10 $\$ $/\$ $/\$ $/\$ $/\$ $\$
195	194	adantlr 712	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
196	195	adantll 711	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
197		difss 3617	. . . . . . . . . . . 12 $\$ $\$
198		ovolsscl 22063	. . . . . . . . . . . 12 $\$ $\$ $/\$ $/\$ $\$ $\$
199	197, 198	mp3an1 1309	. . . . . . . . . . 11 $/\$ $\$ $\$
200	199	ad5antr 731	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
201		simp-6r 770	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
202		simpl 455	. . . . . . . . . . 11 $/\$
203	202	ad4antlr 730	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
204		difdif2 3752	. . . . . . . . . . . 12 $\$ $\$ $\$
205	204	fveq2i 5851	. . . . . . . . . . 11 $\$ $\$ $\$
206		difss 3617	. . . . . . . . . . . . . . 15 $\$
207		inss1 3704	. . . . . . . . . . . . . . 15
208	206, 207	unssi 3665	. . . . . . . . . . . . . 14 $\$
209		ovolsscl 22063	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$
210	208, 209	mp3an1 1309	. . . . . . . . . . . . 13 $/\$ $\$
211	210	ad5antr 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
212		ovolsscl 22063	. . . . . . . . . . . . . . 15 $\$ $/\$ $/\$ $\$
213	206, 212	mp3an1 1309	. . . . . . . . . . . . . 14 $/\$ $\$
214	213	ad5antr 731	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
215		ovolsscl 22063	. . . . . . . . . . . . . . 15 $/\$ $/\$
216	207, 215	mp3an1 1309	. . . . . . . . . . . . . 14 $/\$
217	216	ad5antr 731	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
218	214, 217	readdcld 9612	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
219	3, 202, 98	syl2an 475	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
220	219	ad3antrrr 727	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
221		ssdifss 3621	. . . . . . . . . . . . . . 15 $\$
222	221	adantr 463	. . . . . . . . . . . . . 14 $/\$ $\$
223		ssinss1 3712	. . . . . . . . . . . . . . 15
224	223	adantr 463	. . . . . . . . . . . . . 14 $/\$
225		ovolun 22076	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
226	222, 213, 224, 216, 225	syl22anc 1227	. . . . . . . . . . . . 13 $/\$ $\$ $\$
227	226	ad5antr 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
228	124	ad2antrr 723	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
229	228	adantr 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
230	150	ad2antrr 723	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
231		simprl 754	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
232	150	adantr 463	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
233		ovolsscl 22063	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
234	64, 233	mp3an2 1310	. . . . . . . . . . . . . . . . 17 $/\$
235	231, 232, 234	syl2anr 476	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$