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 31894

Description: Backward direction of ismblfin 31895. (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 9715	. . . 4
2	1	a1i 11	. . 3 $/\$ $/\$
3		simplr 760	. . 3 $/\$ $/\$
4		vex 3084	. . . . . . 7
5		eqeq1 2426	. . . . . . . . 9
6	5	anbi2d 708	. . . . . . . 8 $/\$ $/\$
7	6	rexbidv 2939	. . . . . . 7 $/\$ $/\$
8	4, 7	elab 3218	. . . . . 6 $/\$ $/\$
9		simprl 762	. . . . . . . . 9 $/\$ $/\$
10		ovolss 22425	. . . . . . . . . . 11 $/\$
11		sstr 3472	. . . . . . . . . . . . 13 $/\$
12		ovolcl 22418	. . . . . . . . . . . . 13
13	11, 12	syl 17	. . . . . . . . . . . 12 $/\$
14		ovolcl 22418	. . . . . . . . . . . . 13
15	14	adantl 467	. . . . . . . . . . . 12 $/\$
16		xrlenlt 9700	. . . . . . . . . . . 12 $/\$
17	13, 15, 16	syl2anc 665	. . . . . . . . . . 11 $/\$
18	10, 17	mpbid 213	. . . . . . . . . 10 $/\$
19	18	ancoms 454	. . . . . . . . 9 $/\$
20	9, 19	sylan2 476	. . . . . . . 8 $/\$ $/\$ $/\$
21		simprrr 773	. . . . . . . . . 10 $/\$ $/\$ $/\$
22		uniretop 21770	. . . . . . . . . . . . . . 15
23	22	cldss 20031	. . . . . . . . . . . . . 14
24		dfss4 3707	. . . . . . . . . . . . . 14 $\$ $\$
25	23, 24	sylib 199	. . . . . . . . . . . . 13 $\$ $\$
26		rembl 22481	. . . . . . . . . . . . . 14
27	22	cldopn 20033	. . . . . . . . . . . . . . 15 $\$
28		opnmbl 22547	. . . . . . . . . . . . . . 15 $\$ $\$
29	27, 28	syl 17	. . . . . . . . . . . . . 14 $\$
30		difmbl 22483	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$
31	26, 29, 30	sylancr 667	. . . . . . . . . . . . 13 $\$ $\$
32	25, 31	eqeltrrd 2511	. . . . . . . . . . . 12
33		mblvol 22471	. . . . . . . . . . . 12
34	32, 33	syl 17	. . . . . . . . . . 11
35	34	ad2antrl 732	. . . . . . . . . 10 $/\$ $/\$ $/\$
36	21, 35	eqtrd 2463	. . . . . . . . 9 $/\$ $/\$ $/\$
37	36	breq2d 4432	. . . . . . . 8 $/\$ $/\$ $/\$
38	20, 37	mtbird 302	. . . . . . 7 $/\$ $/\$ $/\$
39	38	rexlimdvaa 2918	. . . . . 6 $/\$
40	8, 39	syl5bi 220	. . . . 5 $/\$
41	40	ad2antrr 730	. . . 4 $/\$ $/\$ $/\$
42	41	imp 430	. . 3 $/\$ $/\$ $/\$ $/\$
43		1rp 11307	. . . . . . . . 9
44		eqid 2422	. . . . . . . . . 10
45	44	ovolgelb 22420	. . . . . . . . 9 $/\$ $/\$ $/\$
46	43, 45	mp3an3 1349	. . . . . . . 8 $/\$ $/\$
47		elmapi 7498	. . . . . . . . . . 11
48		ssid 3483	. . . . . . . . . . . . . . 15
49	44	ovollb 22419	. . . . . . . . . . . . . . 15 $/\$
50	48, 49	mpan2 675	. . . . . . . . . . . . . 14
51	50	adantl 467	. . . . . . . . . . . . 13 $/\$
52		eqid 2422	. . . . . . . . . . . . . . . 16
53	52, 44	ovolsf 22412	. . . . . . . . . . . . . . 15
54		frn 5749	. . . . . . . . . . . . . . . 16
55		icossxr 11720	. . . . . . . . . . . . . . . 16
56	54, 55	syl6ss 3476	. . . . . . . . . . . . . . 15
57		supxrcl 11601	. . . . . . . . . . . . . . 15
58	53, 56, 57	3syl 18	. . . . . . . . . . . . . 14
59		peano2re 9807	. . . . . . . . . . . . . . 15
60	59	rexrd 9691	. . . . . . . . . . . . . 14
61		rncoss 5111	. . . . . . . . . . . . . . . . . 18
62	61	unissi 4239	. . . . . . . . . . . . . . . . 17
63		unirnioo 11735	. . . . . . . . . . . . . . . . 17
64	62, 63	sseqtr4i 3497	. . . . . . . . . . . . . . . 16
65		ovolcl 22418	. . . . . . . . . . . . . . . 16
66	64, 65	ax-mp 5	. . . . . . . . . . . . . . 15
67		xrletr 11456	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
68	66, 67	mp3an1 1347	. . . . . . . . . . . . . 14 $/\$ $/\$
69	58, 60, 68	syl2anr 480	. . . . . . . . . . . . 13 $/\$ $/\$
70	51, 69	mpand 679	. . . . . . . . . . . 12 $/\$
71	70	adantll 718	. . . . . . . . . . 11 $/\$ $/\$
72	47, 71	sylan2 476	. . . . . . . . . 10 $/\$ $/\$
73	72	anim2d 567	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74	73	reximdva 2900	. . . . . . . 8 $/\$ $/\$ $/\$
75	46, 74	mpd 15	. . . . . . 7 $/\$ $/\$
76		rexex 2882	. . . . . . 7 $/\$ $/\$
77	75, 76	syl 17	. . . . . 6 $/\$ $/\$
78	77	ad2antrr 730	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
79		difss 3592	. . . . . . . . . . . . . 14 $\$
80	79, 64	sstri 3473	. . . . . . . . . . . . 13 $\$
81		ovolcl 22418	. . . . . . . . . . . . 13 $\$ $\$
82	80, 81	ax-mp 5	. . . . . . . . . . . 12 $\$
83	59, 82	jctil 539	. . . . . . . . . . 11 $\$ $/\$
84	83	ad4antlr 737	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
85		ovolss 22425	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
86	79, 64, 85	mp2an 676	. . . . . . . . . . . . . 14 $\$
87		xrletr 11456	. . . . . . . . . . . . . . . 16 $\$ $/\$ $/\$ $\$ $/\$ $\$
88	82, 66, 87	mp3an12 1350	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
89	60, 88	syl 17	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
90	86, 89	mpani 680	. . . . . . . . . . . . 13 $\$
91	90	ad4antlr 737	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
92	91	impr 623	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
93		ovolge0 22421	. . . . . . . . . . . 12 $\$ $\$
94	80, 93	ax-mp 5	. . . . . . . . . . 11 $\$
95	92, 94	jctil 539	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
96		xrrege0 11470	. . . . . . . . . 10 $\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
97	84, 95, 96	syl2anc 665	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
98		resubcl 9939	. . . . . . . . . . . . . 14 $/\$
99	98	adantrr 721	. . . . . . . . . . . . 13 $/\$ $/\$
100		posdif 10108	. . . . . . . . . . . . . . . 16 $/\$
101	100	ancoms 454	. . . . . . . . . . . . . . 15 $/\$
102	101	biimpd 210	. . . . . . . . . . . . . 14 $/\$
103	102	impr 623	. . . . . . . . . . . . 13 $/\$ $/\$
104	99, 103	elrpd 11339	. . . . . . . . . . . 12 $/\$ $/\$
105	104	rphalfcld 11354	. . . . . . . . . . 11 $/\$ $/\$
106	3, 105	sylan 473	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
107	106	adantr 466	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		eqid 2422	. . . . . . . . . . 11
109	108	ovolgelb 22420	. . . . . . . . . 10 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
110	80, 109	mp3an1 1347	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$
111	97, 107, 110	syl2anc 665	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
112		elmapi 7498	. . . . . . . . . . 11
113		ssid 3483	. . . . . . . . . . . . . 14
114	108	ovollb 22419	. . . . . . . . . . . . . 14 $/\$
115	113, 114	mpan2 675	. . . . . . . . . . . . 13
116	115	adantl 467	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
117		eqid 2422	. . . . . . . . . . . . . . 15
118	117, 108	ovolsf 22412	. . . . . . . . . . . . . 14
119		frn 5749	. . . . . . . . . . . . . . 15
120	119, 55	syl6ss 3476	. . . . . . . . . . . . . 14
121		supxrcl 11601	. . . . . . . . . . . . . 14
122	118, 120, 121	3syl 18	. . . . . . . . . . . . 13
123	99	rehalfcld 10860	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
124	3, 123	sylan 473	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
125	124	adantr 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	97, 125	readdcld 9671	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
127	126	rexrd 9691	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
128		rncoss 5111	. . . . . . . . . . . . . . . . 17
129	128	unissi 4239	. . . . . . . . . . . . . . . 16
130	129, 63	sseqtr4i 3497	. . . . . . . . . . . . . . 15
131		ovolcl 22418	. . . . . . . . . . . . . . 15
132	130, 131	ax-mp 5	. . . . . . . . . . . . . 14
133		xrletr 11456	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $\$ $\$
134	132, 133	mp3an1 1347	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$
135	122, 127, 134	syl2anr 480	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
136	116, 135	mpand 679	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
137	112, 136	sylan2 476	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
138	137	anim2d 567	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
139	138	reximdva 2900	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
140	111, 139	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
141		rexex 2882	. . . . . . 7 $\$ $/\$ $\$ $\$ $/\$ $\$
142	140, 141	syl 17	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
143	59, 66	jctil 539	. . . . . . . . . . . 12 $/\$
144	143	ad3antlr 735	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
145		ovolge0 22421	. . . . . . . . . . . . . 14
146	64, 145	ax-mp 5	. . . . . . . . . . . . 13
147	146	jctl 543	. . . . . . . . . . . 12 $/\$
148	147	adantl 467	. . . . . . . . . . 11 $/\$ $/\$
149		xrrege0 11470	. . . . . . . . . . 11 $/\$ $/\$ $/\$
150	144, 148, 149	syl2an 479	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
151	150, 125	resubcld 10048	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
152	150, 107	ltsubrpd 11371	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
153		retop 21769	. . . . . . . . . . 11
154		retopbas 21768	. . . . . . . . . . . . 13
155		bastg 19968	. . . . . . . . . . . . 13
156	154, 155	ax-mp 5	. . . . . . . . . . . 12
157	61, 156	sstri 3473	. . . . . . . . . . 11
158		uniopn 19914	. . . . . . . . . . 11 $/\$
159	153, 157, 158	mp2an 676	. . . . . . . . . 10
160		mblfinlem2 31892	. . . . . . . . . 10 $/\$ $/\$ $/\$
161	159, 160	mp3an1 1347	. . . . . . . . 9 $/\$ $/\$
162	151, 152, 161	syl2anc 665	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	162	adantr 466	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
164		indif2 3716	. . . . . . . . . . . . . . 15 $\$ $\$
165	22	cldss 20031	. . . . . . . . . . . . . . . . 17
166		df-ss 3450	. . . . . . . . . . . . . . . . 17
167	165, 166	sylib 199	. . . . . . . . . . . . . . . 16
168	167	difeq1d 3582	. . . . . . . . . . . . . . 15 $\$ $\$
169	164, 168	syl5eq 2475	. . . . . . . . . . . . . 14 $\$ $\$
170	128, 156	sstri 3473	. . . . . . . . . . . . . . . . 17
171		uniopn 19914	. . . . . . . . . . . . . . . . 17 $/\$
172	153, 170, 171	mp2an 676	. . . . . . . . . . . . . . . 16
173	22	opncld 20035	. . . . . . . . . . . . . . . 16 $/\$ $\$
174	153, 172, 173	mp2an 676	. . . . . . . . . . . . . . 15 $\$
175		incld 20045	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
176	174, 175	mpan2 675	. . . . . . . . . . . . . 14 $\$
177	169, 176	eqeltrrd 2511	. . . . . . . . . . . . 13 $\$
178		simpr 462	. . . . . . . . . . . . . . 15 $\$ $/\$
179		simpl 458	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
180	178, 179	ssdif2d 3604	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
181		dfin4 3713	. . . . . . . . . . . . . . 15 $\$ $\$
182		inss2 3683	. . . . . . . . . . . . . . 15
183	181, 182	eqsstr3i 3495	. . . . . . . . . . . . . 14 $\$ $\$
184	180, 183	syl6ss 3476	. . . . . . . . . . . . 13 $\$ $/\$ $\$
185		sseq1 3485	. . . . . . . . . . . . . . . 16 $\$ $\$
186	185	anbi1d 709	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $\$ $/\$ $\$
187		fveq2 5878	. . . . . . . . . . . . . . . . 17 $\$ $\$
188	187	eqcoms 2434	. . . . . . . . . . . . . . . 16 $\$ $\$
189	188	biantrud 509	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $/\$ $\$
190	186, 189	bitr4d 259	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$
191	190	rspcev 3182	. . . . . . . . . . . . 13 $\$ $/\$ $\$ $/\$ $\$
192	177, 184, 191	syl2an 479	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $/\$ $\$
193	192	an12s 808	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$
194	193	adantrrr 729	. . . . . . . . . 10 $\$ $/\$ $/\$ $/\$ $/\$ $\$
195	194	adantlr 719	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
196	195	adantll 718	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
197		difss 3592	. . . . . . . . . . . 12 $\$ $\$
198		ovolsscl 22426	. . . . . . . . . . . 12 $\$ $\$ $/\$ $/\$ $\$ $\$
199	197, 198	mp3an1 1347	. . . . . . . . . . 11 $/\$ $\$ $\$
200	199	ad5antr 738	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
201		simp-6r 779	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
202		simpl 458	. . . . . . . . . . 11 $/\$
203	202	ad4antlr 737	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
204		difdif2 3730	. . . . . . . . . . . 12 $\$ $\$ $\$
205	204	fveq2i 5881	. . . . . . . . . . 11 $\$ $\$ $\$
206		difss 3592	. . . . . . . . . . . . . . 15 $\$
207		inss1 3682	. . . . . . . . . . . . . . 15
208	206, 207	unssi 3641	. . . . . . . . . . . . . 14 $\$
209		ovolsscl 22426	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$
210	208, 209	mp3an1 1347	. . . . . . . . . . . . 13 $/\$ $\$
211	210	ad5antr 738	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
212		ovolsscl 22426	. . . . . . . . . . . . . . 15 $\$ $/\$ $/\$ $\$
213	206, 212	mp3an1 1347	. . . . . . . . . . . . . 14 $/\$ $\$
214	213	ad5antr 738	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
215		ovolsscl 22426	. . . . . . . . . . . . . . 15 $/\$ $/\$
216	207, 215	mp3an1 1347	. . . . . . . . . . . . . 14 $/\$
217	216	ad5antr 738	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
218	214, 217	readdcld 9671	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
219	3, 202, 98	syl2an 479	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
220	219	ad3antrrr 734	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
221		ssdifss 3596	. . . . . . . . . . . . . . 15 $\$
222	221	adantr 466	. . . . . . . . . . . . . 14 $/\$ $\$
223		ssinss1 3690	. . . . . . . . . . . . . . 15
224	223	adantr 466	. . . . . . . . . . . . . 14 $/\$
225		ovolun 22439	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
226	222, 213, 224, 216, 225	syl22anc 1265	. . . . . . . . . . . . 13 $/\$ $\$ $\$
227	226	ad5antr 738	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
228	124	ad2antrr 730	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
229	228	adantr 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
230	150	ad2antrr 730	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
231		simprl 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
232	150	adantr 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
233		ovolsscl 22426	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
234	64, 233	mp3an2 1348	. . . . . . . . . . . . . . . . 17 $/\$
235	231, 232, 234	syl2anr 480	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$