mblfinlem4 - Mathbox for Brendan Leahy

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

Theorem mblfinlem4 31980

Description: Backward direction of ismblfin 31981. (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 9714	. . . 4
2	1	a1i 11	. . 3 $/\$ $/\$
3		simplr 762	. . 3 $/\$ $/\$
4		vex 3048	. . . . . . 7
5		eqeq1 2455	. . . . . . . . 9
6	5	anbi2d 710	. . . . . . . 8 $/\$ $/\$
7	6	rexbidv 2901	. . . . . . 7 $/\$ $/\$
8	4, 7	elab 3185	. . . . . 6 $/\$ $/\$
9		simprl 764	. . . . . . . . 9 $/\$ $/\$
10		ovolss 22438	. . . . . . . . . . 11 $/\$
11		sstr 3440	. . . . . . . . . . . . 13 $/\$
12		ovolcl 22431	. . . . . . . . . . . . 13
13	11, 12	syl 17	. . . . . . . . . . . 12 $/\$
14		ovolcl 22431	. . . . . . . . . . . . 13
15	14	adantl 468	. . . . . . . . . . . 12 $/\$
16		xrlenlt 9699	. . . . . . . . . . . 12 $/\$
17	13, 15, 16	syl2anc 667	. . . . . . . . . . 11 $/\$
18	10, 17	mpbid 214	. . . . . . . . . 10 $/\$
19	18	ancoms 455	. . . . . . . . 9 $/\$
20	9, 19	sylan2 477	. . . . . . . 8 $/\$ $/\$ $/\$
21		simprrr 775	. . . . . . . . . 10 $/\$ $/\$ $/\$
22		uniretop 21783	. . . . . . . . . . . . . . 15
23	22	cldss 20044	. . . . . . . . . . . . . 14
24		dfss4 3677	. . . . . . . . . . . . . 14 $\$ $\$
25	23, 24	sylib 200	. . . . . . . . . . . . 13 $\$ $\$
26		rembl 22494	. . . . . . . . . . . . . 14
27	22	cldopn 20046	. . . . . . . . . . . . . . 15 $\$
28		opnmbl 22560	. . . . . . . . . . . . . . 15 $\$ $\$
29	27, 28	syl 17	. . . . . . . . . . . . . 14 $\$
30		difmbl 22496	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$
31	26, 29, 30	sylancr 669	. . . . . . . . . . . . 13 $\$ $\$
32	25, 31	eqeltrrd 2530	. . . . . . . . . . . 12
33		mblvol 22484	. . . . . . . . . . . 12
34	32, 33	syl 17	. . . . . . . . . . 11
35	34	ad2antrl 734	. . . . . . . . . 10 $/\$ $/\$ $/\$
36	21, 35	eqtrd 2485	. . . . . . . . 9 $/\$ $/\$ $/\$
37	36	breq2d 4414	. . . . . . . 8 $/\$ $/\$ $/\$
38	20, 37	mtbird 303	. . . . . . 7 $/\$ $/\$ $/\$
39	38	rexlimdvaa 2880	. . . . . 6 $/\$
40	8, 39	syl5bi 221	. . . . 5 $/\$
41	40	ad2antrr 732	. . . 4 $/\$ $/\$ $/\$
42	41	imp 431	. . 3 $/\$ $/\$ $/\$ $/\$
43		1rp 11306	. . . . . . . . 9
44		eqid 2451	. . . . . . . . . 10
45	44	ovolgelb 22433	. . . . . . . . 9 $/\$ $/\$ $/\$
46	43, 45	mp3an3 1353	. . . . . . . 8 $/\$ $/\$
47		elmapi 7493	. . . . . . . . . . 11
48		ssid 3451	. . . . . . . . . . . . . . 15
49	44	ovollb 22432	. . . . . . . . . . . . . . 15 $/\$
50	48, 49	mpan2 677	. . . . . . . . . . . . . 14
51	50	adantl 468	. . . . . . . . . . . . 13 $/\$
52		eqid 2451	. . . . . . . . . . . . . . . 16
53	52, 44	ovolsf 22425	. . . . . . . . . . . . . . 15
54		frn 5735	. . . . . . . . . . . . . . . 16
55		icossxr 11719	. . . . . . . . . . . . . . . 16
56	54, 55	syl6ss 3444	. . . . . . . . . . . . . . 15
57		supxrcl 11600	. . . . . . . . . . . . . . 15
58	53, 56, 57	3syl 18	. . . . . . . . . . . . . 14
59		peano2re 9806	. . . . . . . . . . . . . . 15
60	59	rexrd 9690	. . . . . . . . . . . . . 14
61		rncoss 5095	. . . . . . . . . . . . . . . . . 18
62	61	unissi 4221	. . . . . . . . . . . . . . . . 17
63		unirnioo 11734	. . . . . . . . . . . . . . . . 17
64	62, 63	sseqtr4i 3465	. . . . . . . . . . . . . . . 16
65		ovolcl 22431	. . . . . . . . . . . . . . . 16
66	64, 65	ax-mp 5	. . . . . . . . . . . . . . 15
67		xrletr 11455	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
68	66, 67	mp3an1 1351	. . . . . . . . . . . . . 14 $/\$ $/\$
69	58, 60, 68	syl2anr 481	. . . . . . . . . . . . 13 $/\$ $/\$
70	51, 69	mpand 681	. . . . . . . . . . . 12 $/\$
71	70	adantll 720	. . . . . . . . . . 11 $/\$ $/\$
72	47, 71	sylan2 477	. . . . . . . . . 10 $/\$ $/\$
73	72	anim2d 569	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74	73	reximdva 2862	. . . . . . . 8 $/\$ $/\$ $/\$
75	46, 74	mpd 15	. . . . . . 7 $/\$ $/\$
76		rexex 2844	. . . . . . 7 $/\$ $/\$
77	75, 76	syl 17	. . . . . 6 $/\$ $/\$
78	77	ad2antrr 732	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
79		difss 3560	. . . . . . . . . . . . . 14 $\$
80	79, 64	sstri 3441	. . . . . . . . . . . . 13 $\$
81		ovolcl 22431	. . . . . . . . . . . . 13 $\$ $\$
82	80, 81	ax-mp 5	. . . . . . . . . . . 12 $\$
83	59, 82	jctil 540	. . . . . . . . . . 11 $\$ $/\$
84	83	ad4antlr 739	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
85		ovolss 22438	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
86	79, 64, 85	mp2an 678	. . . . . . . . . . . . . 14 $\$
87		xrletr 11455	. . . . . . . . . . . . . . . 16 $\$ $/\$ $/\$ $\$ $/\$ $\$
88	82, 66, 87	mp3an12 1354	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
89	60, 88	syl 17	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
90	86, 89	mpani 682	. . . . . . . . . . . . 13 $\$
91	90	ad4antlr 739	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
92	91	impr 625	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
93		ovolge0 22434	. . . . . . . . . . . 12 $\$ $\$
94	80, 93	ax-mp 5	. . . . . . . . . . 11 $\$
95	92, 94	jctil 540	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
96		xrrege0 11469	. . . . . . . . . 10 $\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
97	84, 95, 96	syl2anc 667	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
98		resubcl 9938	. . . . . . . . . . . . . 14 $/\$
99	98	adantrr 723	. . . . . . . . . . . . 13 $/\$ $/\$
100		posdif 10107	. . . . . . . . . . . . . . . 16 $/\$
101	100	ancoms 455	. . . . . . . . . . . . . . 15 $/\$
102	101	biimpd 211	. . . . . . . . . . . . . 14 $/\$
103	102	impr 625	. . . . . . . . . . . . 13 $/\$ $/\$
104	99, 103	elrpd 11338	. . . . . . . . . . . 12 $/\$ $/\$
105	104	rphalfcld 11353	. . . . . . . . . . 11 $/\$ $/\$
106	3, 105	sylan 474	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
107	106	adantr 467	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		eqid 2451	. . . . . . . . . . 11
109	108	ovolgelb 22433	. . . . . . . . . 10 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
110	80, 109	mp3an1 1351	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$
111	97, 107, 110	syl2anc 667	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
112		elmapi 7493	. . . . . . . . . . 11
113		ssid 3451	. . . . . . . . . . . . . 14
114	108	ovollb 22432	. . . . . . . . . . . . . 14 $/\$
115	113, 114	mpan2 677	. . . . . . . . . . . . 13
116	115	adantl 468	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
117		eqid 2451	. . . . . . . . . . . . . . 15
118	117, 108	ovolsf 22425	. . . . . . . . . . . . . 14
119		frn 5735	. . . . . . . . . . . . . . 15
120	119, 55	syl6ss 3444	. . . . . . . . . . . . . 14
121		supxrcl 11600	. . . . . . . . . . . . . 14
122	118, 120, 121	3syl 18	. . . . . . . . . . . . 13
123	99	rehalfcld 10859	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
124	3, 123	sylan 474	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
125	124	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	97, 125	readdcld 9670	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
127	126	rexrd 9690	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
128		rncoss 5095	. . . . . . . . . . . . . . . . 17
129	128	unissi 4221	. . . . . . . . . . . . . . . 16
130	129, 63	sseqtr4i 3465	. . . . . . . . . . . . . . 15
131		ovolcl 22431	. . . . . . . . . . . . . . 15
132	130, 131	ax-mp 5	. . . . . . . . . . . . . 14
133		xrletr 11455	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $\$ $\$
134	132, 133	mp3an1 1351	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$
135	122, 127, 134	syl2anr 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
136	116, 135	mpand 681	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
137	112, 136	sylan2 477	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
138	137	anim2d 569	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
139	138	reximdva 2862	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
140	111, 139	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
141		rexex 2844	. . . . . . 7 $\$ $/\$ $\$ $\$ $/\$ $\$
142	140, 141	syl 17	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
143	59, 66	jctil 540	. . . . . . . . . . . 12 $/\$
144	143	ad3antlr 737	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
145		ovolge0 22434	. . . . . . . . . . . . . 14
146	64, 145	ax-mp 5	. . . . . . . . . . . . 13
147	146	jctl 544	. . . . . . . . . . . 12 $/\$
148	147	adantl 468	. . . . . . . . . . 11 $/\$ $/\$
149		xrrege0 11469	. . . . . . . . . . 11 $/\$ $/\$ $/\$
150	144, 148, 149	syl2an 480	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
151	150, 125	resubcld 10047	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
152	150, 107	ltsubrpd 11370	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
153		retop 21782	. . . . . . . . . . 11
154		retopbas 21781	. . . . . . . . . . . . 13
155		bastg 19981	. . . . . . . . . . . . 13
156	154, 155	ax-mp 5	. . . . . . . . . . . 12
157	61, 156	sstri 3441	. . . . . . . . . . 11
158		uniopn 19927	. . . . . . . . . . 11 $/\$
159	153, 157, 158	mp2an 678	. . . . . . . . . 10
160		mblfinlem2 31978	. . . . . . . . . 10 $/\$ $/\$ $/\$
161	159, 160	mp3an1 1351	. . . . . . . . 9 $/\$ $/\$
162	151, 152, 161	syl2anc 667	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	162	adantr 467	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
164		indif2 3686	. . . . . . . . . . . . . . 15 $\$ $\$
165	22	cldss 20044	. . . . . . . . . . . . . . . . 17
166		df-ss 3418	. . . . . . . . . . . . . . . . 17
167	165, 166	sylib 200	. . . . . . . . . . . . . . . 16
168	167	difeq1d 3550	. . . . . . . . . . . . . . 15 $\$ $\$
169	164, 168	syl5eq 2497	. . . . . . . . . . . . . 14 $\$ $\$
170	128, 156	sstri 3441	. . . . . . . . . . . . . . . . 17
171		uniopn 19927	. . . . . . . . . . . . . . . . 17 $/\$
172	153, 170, 171	mp2an 678	. . . . . . . . . . . . . . . 16
173	22	opncld 20048	. . . . . . . . . . . . . . . 16 $/\$ $\$
174	153, 172, 173	mp2an 678	. . . . . . . . . . . . . . 15 $\$
175		incld 20058	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
176	174, 175	mpan2 677	. . . . . . . . . . . . . 14 $\$
177	169, 176	eqeltrrd 2530	. . . . . . . . . . . . 13 $\$
178		simpr 463	. . . . . . . . . . . . . . 15 $\$ $/\$
179		simpl 459	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
180	178, 179	ssdif2d 3572	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
181		dfin4 3683	. . . . . . . . . . . . . . 15 $\$ $\$
182		inss2 3653	. . . . . . . . . . . . . . 15
183	181, 182	eqsstr3i 3463	. . . . . . . . . . . . . 14 $\$ $\$
184	180, 183	syl6ss 3444	. . . . . . . . . . . . 13 $\$ $/\$ $\$
185		sseq1 3453	. . . . . . . . . . . . . . . 16 $\$ $\$
186	185	anbi1d 711	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $\$ $/\$ $\$
187		fveq2 5865	. . . . . . . . . . . . . . . . 17 $\$ $\$
188	187	eqcoms 2459	. . . . . . . . . . . . . . . 16 $\$ $\$
189	188	biantrud 510	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $/\$ $\$
190	186, 189	bitr4d 260	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$
191	190	rspcev 3150	. . . . . . . . . . . . 13 $\$ $/\$ $\$ $/\$ $\$
192	177, 184, 191	syl2an 480	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $/\$ $\$
193	192	an12s 810	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$
194	193	adantrrr 731	. . . . . . . . . 10 $\$ $/\$ $/\$ $/\$ $/\$ $\$
195	194	adantlr 721	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
196	195	adantll 720	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
197		difss 3560	. . . . . . . . . . . 12 $\$ $\$
198		ovolsscl 22439	. . . . . . . . . . . 12 $\$ $\$ $/\$ $/\$ $\$ $\$
199	197, 198	mp3an1 1351	. . . . . . . . . . 11 $/\$ $\$ $\$
200	199	ad5antr 740	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
201		simp-6r 781	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
202		simpl 459	. . . . . . . . . . 11 $/\$
203	202	ad4antlr 739	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
204		difdif2 3700	. . . . . . . . . . . 12 $\$ $\$ $\$
205	204	fveq2i 5868	. . . . . . . . . . 11 $\$ $\$ $\$
206		difss 3560	. . . . . . . . . . . . . . 15 $\$
207		inss1 3652	. . . . . . . . . . . . . . 15
208	206, 207	unssi 3609	. . . . . . . . . . . . . 14 $\$
209		ovolsscl 22439	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$
210	208, 209	mp3an1 1351	. . . . . . . . . . . . 13 $/\$ $\$
211	210	ad5antr 740	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
212		ovolsscl 22439	. . . . . . . . . . . . . . 15 $\$ $/\$ $/\$ $\$
213	206, 212	mp3an1 1351	. . . . . . . . . . . . . 14 $/\$ $\$
214	213	ad5antr 740	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
215		ovolsscl 22439	. . . . . . . . . . . . . . 15 $/\$ $/\$
216	207, 215	mp3an1 1351	. . . . . . . . . . . . . 14 $/\$
217	216	ad5antr 740	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
218	214, 217	readdcld 9670	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
219	3, 202, 98	syl2an 480	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
220	219	ad3antrrr 736	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
221		ssdifss 3564	. . . . . . . . . . . . . . 15 $\$
222	221	adantr 467	. . . . . . . . . . . . . 14 $/\$ $\$
223		ssinss1 3660	. . . . . . . . . . . . . . 15
224	223	adantr 467	. . . . . . . . . . . . . 14 $/\$
225		ovolun 22452	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
226	222, 213, 224, 216, 225	syl22anc 1269	. . . . . . . . . . . . 13 $/\$ $\$ $\$
227	226	ad5antr 740	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
228	124	ad2antrr 732	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
229	228	adantr 467	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
230	150	ad2antrr 732	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
231		simprl 764	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
232	150	adantr 467	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
233		ovolsscl 22439	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
234	64, 233	mp3an2 1352	. . . . . . . . . . . . . . . . 17 $/\$
235	231, 232, 234	syl2anr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$