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 32044

Description: Backward direction of ismblfin 32045. (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 9732	. . . 4
2	1	a1i 11	. . 3 $/\$ $/\$
3		simplr 770	. . 3 $/\$ $/\$
4		vex 3034	. . . . . . 7
5		eqeq1 2475	. . . . . . . . 9
6	5	anbi2d 718	. . . . . . . 8 $/\$ $/\$
7	6	rexbidv 2892	. . . . . . 7 $/\$ $/\$
8	4, 7	elab 3173	. . . . . 6 $/\$ $/\$
9		simprl 772	. . . . . . . . 9 $/\$ $/\$
10		ovolss 22516	. . . . . . . . . . 11 $/\$
11		sstr 3426	. . . . . . . . . . . . 13 $/\$
12		ovolcl 22509	. . . . . . . . . . . . 13
13	11, 12	syl 17	. . . . . . . . . . . 12 $/\$
14		ovolcl 22509	. . . . . . . . . . . . 13
15	14	adantl 473	. . . . . . . . . . . 12 $/\$
16		xrlenlt 9717	. . . . . . . . . . . 12 $/\$
17	13, 15, 16	syl2anc 673	. . . . . . . . . . 11 $/\$
18	10, 17	mpbid 215	. . . . . . . . . 10 $/\$
19	18	ancoms 460	. . . . . . . . 9 $/\$
20	9, 19	sylan2 482	. . . . . . . 8 $/\$ $/\$ $/\$
21		simprrr 783	. . . . . . . . . 10 $/\$ $/\$ $/\$
22		uniretop 21861	. . . . . . . . . . . . . . 15
23	22	cldss 20121	. . . . . . . . . . . . . 14
24		dfss4 3668	. . . . . . . . . . . . . 14 $\$ $\$
25	23, 24	sylib 201	. . . . . . . . . . . . 13 $\$ $\$
26		rembl 22572	. . . . . . . . . . . . . 14
27	22	cldopn 20123	. . . . . . . . . . . . . . 15 $\$
28		opnmbl 22639	. . . . . . . . . . . . . . 15 $\$ $\$
29	27, 28	syl 17	. . . . . . . . . . . . . 14 $\$
30		difmbl 22575	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$
31	26, 29, 30	sylancr 676	. . . . . . . . . . . . 13 $\$ $\$
32	25, 31	eqeltrrd 2550	. . . . . . . . . . . 12
33		mblvol 22562	. . . . . . . . . . . 12
34	32, 33	syl 17	. . . . . . . . . . 11
35	34	ad2antrl 742	. . . . . . . . . 10 $/\$ $/\$ $/\$
36	21, 35	eqtrd 2505	. . . . . . . . 9 $/\$ $/\$ $/\$
37	36	breq2d 4407	. . . . . . . 8 $/\$ $/\$ $/\$
38	20, 37	mtbird 308	. . . . . . 7 $/\$ $/\$ $/\$
39	38	rexlimdvaa 2872	. . . . . 6 $/\$
40	8, 39	syl5bi 225	. . . . 5 $/\$
41	40	ad2antrr 740	. . . 4 $/\$ $/\$ $/\$
42	41	imp 436	. . 3 $/\$ $/\$ $/\$ $/\$
43		1rp 11329	. . . . . . . . 9
44		eqid 2471	. . . . . . . . . 10
45	44	ovolgelb 22511	. . . . . . . . 9 $/\$ $/\$ $/\$
46	43, 45	mp3an3 1379	. . . . . . . 8 $/\$ $/\$
47		elmapi 7511	. . . . . . . . . . 11
48		ssid 3437	. . . . . . . . . . . . . . 15
49	44	ovollb 22510	. . . . . . . . . . . . . . 15 $/\$
50	48, 49	mpan2 685	. . . . . . . . . . . . . 14
51	50	adantl 473	. . . . . . . . . . . . 13 $/\$
52		eqid 2471	. . . . . . . . . . . . . . . 16
53	52, 44	ovolsf 22503	. . . . . . . . . . . . . . 15
54		frn 5747	. . . . . . . . . . . . . . . 16
55		icossxr 11744	. . . . . . . . . . . . . . . 16
56	54, 55	syl6ss 3430	. . . . . . . . . . . . . . 15
57		supxrcl 11625	. . . . . . . . . . . . . . 15
58	53, 56, 57	3syl 18	. . . . . . . . . . . . . 14
59		peano2re 9824	. . . . . . . . . . . . . . 15
60	59	rexrd 9708	. . . . . . . . . . . . . 14
61		rncoss 5101	. . . . . . . . . . . . . . . . . 18
62	61	unissi 4213	. . . . . . . . . . . . . . . . 17
63		unirnioo 11759	. . . . . . . . . . . . . . . . 17
64	62, 63	sseqtr4i 3451	. . . . . . . . . . . . . . . 16
65		ovolcl 22509	. . . . . . . . . . . . . . . 16
66	64, 65	ax-mp 5	. . . . . . . . . . . . . . 15
67		xrletr 11478	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
68	66, 67	mp3an1 1377	. . . . . . . . . . . . . 14 $/\$ $/\$
69	58, 60, 68	syl2anr 486	. . . . . . . . . . . . 13 $/\$ $/\$
70	51, 69	mpand 689	. . . . . . . . . . . 12 $/\$
71	70	adantll 728	. . . . . . . . . . 11 $/\$ $/\$
72	47, 71	sylan2 482	. . . . . . . . . 10 $/\$ $/\$
73	72	anim2d 575	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
74	73	reximdva 2858	. . . . . . . 8 $/\$ $/\$ $/\$
75	46, 74	mpd 15	. . . . . . 7 $/\$ $/\$
76		rexex 2843	. . . . . . 7 $/\$ $/\$
77	75, 76	syl 17	. . . . . 6 $/\$ $/\$
78	77	ad2antrr 740	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
79		difss 3549	. . . . . . . . . . . . . 14 $\$
80	79, 64	sstri 3427	. . . . . . . . . . . . 13 $\$
81		ovolcl 22509	. . . . . . . . . . . . 13 $\$ $\$
82	80, 81	ax-mp 5	. . . . . . . . . . . 12 $\$
83	59, 82	jctil 546	. . . . . . . . . . 11 $\$ $/\$
84	83	ad4antlr 747	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
85		ovolss 22516	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
86	79, 64, 85	mp2an 686	. . . . . . . . . . . . . 14 $\$
87		xrletr 11478	. . . . . . . . . . . . . . . 16 $\$ $/\$ $/\$ $\$ $/\$ $\$
88	82, 66, 87	mp3an12 1380	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
89	60, 88	syl 17	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
90	86, 89	mpani 690	. . . . . . . . . . . . 13 $\$
91	90	ad4antlr 747	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
92	91	impr 631	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
93		ovolge0 22512	. . . . . . . . . . . 12 $\$ $\$
94	80, 93	ax-mp 5	. . . . . . . . . . 11 $\$
95	92, 94	jctil 546	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
96		xrrege0 11492	. . . . . . . . . 10 $\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
97	84, 95, 96	syl2anc 673	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
98		resubcl 9958	. . . . . . . . . . . . . 14 $/\$
99	98	adantrr 731	. . . . . . . . . . . . 13 $/\$ $/\$
100		posdif 10128	. . . . . . . . . . . . . . . 16 $/\$
101	100	ancoms 460	. . . . . . . . . . . . . . 15 $/\$
102	101	biimpd 212	. . . . . . . . . . . . . 14 $/\$
103	102	impr 631	. . . . . . . . . . . . 13 $/\$ $/\$
104	99, 103	elrpd 11361	. . . . . . . . . . . 12 $/\$ $/\$
105	104	rphalfcld 11376	. . . . . . . . . . 11 $/\$ $/\$
106	3, 105	sylan 479	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
107	106	adantr 472	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		eqid 2471	. . . . . . . . . . 11
109	108	ovolgelb 22511	. . . . . . . . . 10 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$
110	80, 109	mp3an1 1377	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $\$
111	97, 107, 110	syl2anc 673	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
112		elmapi 7511	. . . . . . . . . . 11
113		ssid 3437	. . . . . . . . . . . . . 14
114	108	ovollb 22510	. . . . . . . . . . . . . 14 $/\$
115	113, 114	mpan2 685	. . . . . . . . . . . . 13
116	115	adantl 473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
117		eqid 2471	. . . . . . . . . . . . . . 15
118	117, 108	ovolsf 22503	. . . . . . . . . . . . . 14
119		frn 5747	. . . . . . . . . . . . . . 15
120	119, 55	syl6ss 3430	. . . . . . . . . . . . . 14
121		supxrcl 11625	. . . . . . . . . . . . . 14
122	118, 120, 121	3syl 18	. . . . . . . . . . . . 13
123	99	rehalfcld 10882	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
124	3, 123	sylan 479	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
125	124	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
126	97, 125	readdcld 9688	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
127	126	rexrd 9708	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
128		rncoss 5101	. . . . . . . . . . . . . . . . 17
129	128	unissi 4213	. . . . . . . . . . . . . . . 16
130	129, 63	sseqtr4i 3451	. . . . . . . . . . . . . . 15
131		ovolcl 22509	. . . . . . . . . . . . . . 15
132	130, 131	ax-mp 5	. . . . . . . . . . . . . 14
133		xrletr 11478	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$ $\$ $\$
134	132, 133	mp3an1 1377	. . . . . . . . . . . . 13 $/\$ $\$ $/\$ $\$ $\$
135	122, 127, 134	syl2anr 486	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
136	116, 135	mpand 689	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
137	112, 136	sylan2 482	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
138	137	anim2d 575	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
139	138	reximdva 2858	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $/\$ $\$
140	111, 139	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
141		rexex 2843	. . . . . . 7 $\$ $/\$ $\$ $\$ $/\$ $\$
142	140, 141	syl 17	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
143	59, 66	jctil 546	. . . . . . . . . . . 12 $/\$
144	143	ad3antlr 745	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
145		ovolge0 22512	. . . . . . . . . . . . . 14
146	64, 145	ax-mp 5	. . . . . . . . . . . . 13
147	146	jctl 550	. . . . . . . . . . . 12 $/\$
148	147	adantl 473	. . . . . . . . . . 11 $/\$ $/\$
149		xrrege0 11492	. . . . . . . . . . 11 $/\$ $/\$ $/\$
150	144, 148, 149	syl2an 485	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
151	150, 125	resubcld 10068	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
152	150, 107	ltsubrpd 11393	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
153		retop 21860	. . . . . . . . . . 11
154		retopbas 21859	. . . . . . . . . . . . 13
155		bastg 20058	. . . . . . . . . . . . 13
156	154, 155	ax-mp 5	. . . . . . . . . . . 12
157	61, 156	sstri 3427	. . . . . . . . . . 11
158		uniopn 20004	. . . . . . . . . . 11 $/\$
159	153, 157, 158	mp2an 686	. . . . . . . . . 10
160		mblfinlem2 32042	. . . . . . . . . 10 $/\$ $/\$ $/\$
161	159, 160	mp3an1 1377	. . . . . . . . 9 $/\$ $/\$
162	151, 152, 161	syl2anc 673	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	162	adantr 472	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
164		indif2 3677	. . . . . . . . . . . . . . 15 $\$ $\$
165	22	cldss 20121	. . . . . . . . . . . . . . . . 17
166		df-ss 3404	. . . . . . . . . . . . . . . . 17
167	165, 166	sylib 201	. . . . . . . . . . . . . . . 16
168	167	difeq1d 3539	. . . . . . . . . . . . . . 15 $\$ $\$
169	164, 168	syl5eq 2517	. . . . . . . . . . . . . 14 $\$ $\$
170	128, 156	sstri 3427	. . . . . . . . . . . . . . . . 17
171		uniopn 20004	. . . . . . . . . . . . . . . . 17 $/\$
172	153, 170, 171	mp2an 686	. . . . . . . . . . . . . . . 16
173	22	opncld 20125	. . . . . . . . . . . . . . . 16 $/\$ $\$
174	153, 172, 173	mp2an 686	. . . . . . . . . . . . . . 15 $\$
175		incld 20135	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
176	174, 175	mpan2 685	. . . . . . . . . . . . . 14 $\$
177	169, 176	eqeltrrd 2550	. . . . . . . . . . . . 13 $\$
178		simpr 468	. . . . . . . . . . . . . . 15 $\$ $/\$
179		simpl 464	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
180	178, 179	ssdif2d 3561	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$ $\$
181		dfin4 3674	. . . . . . . . . . . . . . 15 $\$ $\$
182		inss2 3644	. . . . . . . . . . . . . . 15
183	181, 182	eqsstr3i 3449	. . . . . . . . . . . . . 14 $\$ $\$
184	180, 183	syl6ss 3430	. . . . . . . . . . . . 13 $\$ $/\$ $\$
185		sseq1 3439	. . . . . . . . . . . . . . . 16 $\$ $\$
186	185	anbi1d 719	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $\$ $/\$ $\$
187		fveq2 5879	. . . . . . . . . . . . . . . . 17 $\$ $\$
188	187	eqcoms 2479	. . . . . . . . . . . . . . . 16 $\$ $\$
189	188	biantrud 515	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $/\$ $\$
190	186, 189	bitr4d 264	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $\$
191	190	rspcev 3136	. . . . . . . . . . . . 13 $\$ $/\$ $\$ $/\$ $\$
192	177, 184, 191	syl2an 485	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $/\$ $\$
193	192	an12s 818	. . . . . . . . . . 11 $\$ $/\$ $/\$ $/\$ $\$
194	193	adantrrr 739	. . . . . . . . . 10 $\$ $/\$ $/\$ $/\$ $/\$ $\$
195	194	adantlr 729	. . . . . . . . 9 $\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
196	195	adantll 728	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$
197		difss 3549	. . . . . . . . . . . 12 $\$ $\$
198		ovolsscl 22517	. . . . . . . . . . . 12 $\$ $\$ $/\$ $/\$ $\$ $\$
199	197, 198	mp3an1 1377	. . . . . . . . . . 11 $/\$ $\$ $\$
200	199	ad5antr 748	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
201		simp-6r 789	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
202		simpl 464	. . . . . . . . . . 11 $/\$
203	202	ad4antlr 747	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
204		difdif2 3691	. . . . . . . . . . . 12 $\$ $\$ $\$
205	204	fveq2i 5882	. . . . . . . . . . 11 $\$ $\$ $\$
206		difss 3549	. . . . . . . . . . . . . . 15 $\$
207		inss1 3643	. . . . . . . . . . . . . . 15
208	206, 207	unssi 3600	. . . . . . . . . . . . . 14 $\$
209		ovolsscl 22517	. . . . . . . . . . . . . 14 $\$ $/\$ $/\$ $\$
210	208, 209	mp3an1 1377	. . . . . . . . . . . . 13 $/\$ $\$
211	210	ad5antr 748	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
212		ovolsscl 22517	. . . . . . . . . . . . . . 15 $\$ $/\$ $/\$ $\$
213	206, 212	mp3an1 1377	. . . . . . . . . . . . . 14 $/\$ $\$
214	213	ad5antr 748	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
215		ovolsscl 22517	. . . . . . . . . . . . . . 15 $/\$ $/\$
216	207, 215	mp3an1 1377	. . . . . . . . . . . . . 14 $/\$
217	216	ad5antr 748	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
218	214, 217	readdcld 9688	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$
219	3, 202, 98	syl2an 485	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
220	219	ad3antrrr 744	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
221		ssdifss 3553	. . . . . . . . . . . . . . 15 $\$
222	221	adantr 472	. . . . . . . . . . . . . 14 $/\$ $\$
223		ssinss1 3651	. . . . . . . . . . . . . . 15
224	223	adantr 472	. . . . . . . . . . . . . 14 $/\$
225		ovolun 22530	. . . . . . . . . . . . . 14 $\$ $/\$ $\$ $/\$ $/\$ $\$ $\$
226	222, 213, 224, 216, 225	syl22anc 1293	. . . . . . . . . . . . 13 $/\$ $\$ $\$
227	226	ad5antr 748	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$
228	124	ad2antrr 740	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
229	228	adantr 472	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
230	150	ad2antrr 740	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
231		simprl 772	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
232	150	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
233		ovolsscl 22517	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
234	64, 233	mp3an2 1378	. . . . . . . . . . . . . . . . 17 $/\$
235	231, 232, 234	syl2anr 486	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$