ismblfin - Mathbox for Brendan Leahy

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

Theorem ismblfin 29660

Description: Measurability in terms of inner and outer measure. Proposition 7 of [Viaclovsky8] p. 3. (Contributed by Brendan Leahy, 4-Mar-2018.) (Revised by Brendan Leahy, 28-Mar-2018.)

**Assertion**
Ref	Expression
ismblfin	$/\$ $/\$

Distinct variable group:

Proof of Theorem ismblfin Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mblfinlem4 29659	. 2 $/\$ $/\$ $/\$
2		elpwi 4019	. . . . 5
3		elmapi 7440	. . . . . . . . . . . 12
4		inss1 3718	. . . . . . . . . . . . . . . . . . . 20
5		ovolsscl 21660	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
6	4, 5	mp3an1 1311	. . . . . . . . . . . . . . . . . . 19 $/\$
7		difss 3631	. . . . . . . . . . . . . . . . . . . 20 $\$
8		ovolsscl 21660	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$
9	7, 8	mp3an1 1311	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
10	6, 9	readdcld 9623	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
11	10	rexrd 9643	. . . . . . . . . . . . . . . . 17 $/\$ $\$
12	11	ad3antlr 730	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
13		rncoss 5263	. . . . . . . . . . . . . . . . . . 19
14	13	unissi 4268	. . . . . . . . . . . . . . . . . 18
15		unirnioo 11624	. . . . . . . . . . . . . . . . . 18
16	14, 15	sseqtr4i 3537	. . . . . . . . . . . . . . . . 17
17		ovolcl 21652	. . . . . . . . . . . . . . . . 17
18	16, 17	mp1i 12	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		eqid 2467	. . . . . . . . . . . . . . . . . . 19
20		eqid 2467	. . . . . . . . . . . . . . . . . . 19
21	19, 20	ovolsf 21647	. . . . . . . . . . . . . . . . . 18
22		frn 5737	. . . . . . . . . . . . . . . . . . 19
23		icossxr 11609	. . . . . . . . . . . . . . . . . . 19
24	22, 23	syl6ss 3516	. . . . . . . . . . . . . . . . . 18
25		supxrcl 11506	. . . . . . . . . . . . . . . . . 18
26	21, 24, 25	3syl 20	. . . . . . . . . . . . . . . . 17
27	26	ad2antlr 726	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		pnfge 11339	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
29	11, 28	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$
30	29	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $\$
31		simpr 461	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
32	30, 31	breqtrrd 4473	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $\$
33	32	adantlll 717	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
34	16, 17	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
35		nltpnft 11367	. . . . . . . . . . . . . . . . . . . . . 22
36	34, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
37	36	necon2abii 2733	. . . . . . . . . . . . . . . . . . . 20
38		ovolge0 21655	. . . . . . . . . . . . . . . . . . . . . 22
39	16, 38	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
40		0re 9596	. . . . . . . . . . . . . . . . . . . . . 22
41		xrre3 11372	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
42	34, 40, 41	mpanl12 682	. . . . . . . . . . . . . . . . . . . . 21 $/\$
43	39, 42	mpan 670	. . . . . . . . . . . . . . . . . . . 20
44	37, 43	sylbir 213	. . . . . . . . . . . . . . . . . . 19
45	10	ad3antlr 730	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
46		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
47		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
48		uniretop 21032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
49	48	cldss 19324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
50		dfss4 3732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
51	49, 50	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
52		rembl 21714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
53	48	cldopn 19326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$
54		opnmbl 21774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$
55	53, 54	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
56		difmbl 21716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $\$ $\$ $\$
57	52, 55, 56	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
58	51, 57	eqeltrrd 2556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
59	47, 58	vtoclga 3177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		mblvol 21704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
61	59, 60	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62	46, 61	sylan9eqr 2530	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
63	62	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
64		inss1 3718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
65		sstr 3512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
66	64, 65	mpan2 671	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	66	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
68		ovolsscl 21660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
69	16, 68	mp3an2 1312	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	69	ancoms 453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
71	67, 70	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
72	63, 71	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
73	72	rexlimdvaa 2956	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
74	73	abssdv 3574	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
75		eqeq1 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
76	75	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
77	76	rexbidv 2973	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
78	77	ralab 3264	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
79		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
80	79, 61	sylan9eqr 2530	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
81		ovolss 21659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
82	66, 16, 81	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
83	82	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
84	80, 83	eqbrtrd 4467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
85	84	rexlimiva 2951	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
86	78, 85	mpgbir 1605	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
87		breq2 4451	. . . . . . . . . . . . . . . . . . . . . . . . . 26
88	87	ralbidv 2903	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
89	88	rspcev 3214	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
90	86, 89	mpan2 671	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
91		retop 21031	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
92		0cld 19333	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
93	91, 92	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
94		0ss 3814	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
95		0mbl 21713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		mblvol 21704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98		ovol0 21667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	97, 98	eqtr2i 2497	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
100	94, 99	pm3.2i 455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
101		sseq1 3525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
103	102	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
104	101, 103	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
105	104	rspcev 3214	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
106	93, 100, 105	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
107		c0ex 9590	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
108		eqeq1 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
109	108	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
110	109	rexbidv 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
111	107, 110	elab 3250	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
112	106, 111	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
113		ne0i 3791	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
114	112, 113	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
115		suprcl 10503	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116	114, 115	mp3an2 1312	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
117	74, 90, 116	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
118		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$
119		eleq1 2539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120	119, 58	vtoclga 3177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121		mblvol 21704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
122	120, 121	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
123	118, 122	sylan9eqr 2530	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
124	123	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
125		difss2 3633	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
126	125	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
127		ovolsscl 21660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
128	16, 127	mp3an2 1312	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
129	128	ancoms 453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
130	126, 129	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
131	124, 130	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
132	131	rexlimdvaa 2956	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
133	132	abssdv 3574	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$
134		eqeq1 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
135	134	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
136	135	rexbidv 2973	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
137	136	ralab 3264	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $/\$
138		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$
139	138, 122	sylan9eqr 2530	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
140		ovolss 21659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
141	125, 16, 140	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
142	141	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
143	139, 142	eqbrtrd 4467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $/\$
144	143	rexlimiva 2951	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
145	137, 144	mpgbir 1605	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
146	87	ralbidv 2903	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $/\$
147	146	rspcev 3214	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $\$ $/\$
148	145, 147	mpan2 671	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$
149		0ss 3814	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
150	149, 99	pm3.2i 455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$
151		sseq1 3525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
152		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
153	152	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
154	151, 153	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
155	154	rspcev 3214	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$ $\$ $/\$
156	93, 150, 155	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$
157		eqeq1 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
158	157	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
159	158	rexbidv 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
160	107, 159	elab 3250	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
161	156, 160	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
162		ne0i 3791	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $/\$
163	161, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
164		suprcl 10503	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
165	163, 164	mp3an2 1312	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
166	133, 148, 165	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
167	117, 166	readdcld 9623	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$
168	167	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
169		simpr 461	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
170	6	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
171	9	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$
172		ovolsscl 21660	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
173	64, 16, 172	mp3an12 1314	. . . . . . . . . . . . . . . . . . . . . . . . 25
174	173	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
175		difss 3631	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
176		ovolsscl 21660	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$ $\$
177	175, 16, 176	mp3an12 1314	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
178	177	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$
179		ssrin 3723	. . . . . . . . . . . . . . . . . . . . . . . . . 26
180	64, 16	sstri 3513	. . . . . . . . . . . . . . . . . . . . . . . . . 26
181		ovolss 21659	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
182	179, 180, 181	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . 25
183	182	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
184		ssdif 3639	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
185	175, 16	sstri 3513	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
186		ovolss 21659	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $/\$ $\$ $\$ $\$
187	184, 185, 186	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
188	187	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$ $\$
189	170, 171, 174, 178, 183, 188	le2addd 10170	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$ $\$
190		dfin4 3738	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
191	190	fveq2i 5869	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
192	191	oveq1i 6294	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$
193	189, 192	syl6breq 4486	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
194	193	adantlll 717	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
195		simpll 753	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
196	190	sseq2i 3529	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
197	196	anbi1i 695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $\$ $/\$
198	197	rexbii 2965	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $\$ $/\$
199	198	abbii 2601	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $\$ $/\$
200	199	supeq1i 7907	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $\$ $/\$
201	16	jctl 541	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
202	201	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
203	177, 185	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$
204	203	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
205		ltso 9665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
206	205	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
207		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
208		vex 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
209		eqeq1 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
210	209	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
211	210	rexbidv 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
212	208, 211	elab 3250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
213	16, 140	mpan2 671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
214	213	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
215	48	cldss 19324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
216		ovolcl 21652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
217	215, 216	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
218		xrlenlt 9652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
219	217, 34, 218	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
220	219	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
221		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
222	221, 122	sylan9eqr 2530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
223		breq2 4451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
224	223	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
225	222, 224	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
226	225	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
227	220, 226	bitr4d 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
228	214, 227	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
229	228	rexlimiva 2951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
230	212, 229	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
231	230	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
232		retopbas 21030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
233		bastg 19262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
234	232, 233	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
235	13, 234	sstri 3513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
236		uniopn 19201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
237	91, 235, 236	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
238		mblfinlem2 29657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
239	237, 238	mp3an1 1311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
240	122	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
241	240	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
242	241	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
243	242	anim2d 565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
244		fvex 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
245		eqeq1 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
246	245	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
247		breq2 4451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
248	246, 247	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
249	244, 248	spcev 3205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
250	249	anasss 647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
251	243, 250	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
252	251	reximia 2930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
253	239, 252	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
254		r19.41v 3014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
255	254	exbii 1644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
256		rexcom4 3133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
257	134	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
258	257	rexbidv 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
259	258	rexab 3266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
260	255, 256, 259	3bitr4i 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
261	253, 260	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
262	261	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
263	206, 207, 231, 262	eqsupd 7917	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
264	263	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
265	264	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
266		sseq1 3525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
267		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
268	267	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
269	266, 268	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
270	269	cbvrexv 3089	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
271	270	abbii 2601	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
272	271	supeq1i 7907	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
273	265, 272	syl6eq 2524	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
274		sseq1 3525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
275	274, 268	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $\$ $/\$
276	275	cbvrexv 3089	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
277	276	abbii 2601	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
278	277	supeq1i 7907	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
279		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
280		eqeq1 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
281	280	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
282	281	rexbidv 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
283		sseq1 3525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
284		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
285	284	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
286	283, 285	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
287	286	cbvrexv 3089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
288	282, 287	syl6bb 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
289	288	cbvabv 2610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
290	289	supeq1i 7907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
291	290	eqeq2i 2485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
292	291	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
293	292	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
294		mblfinlem3 29658	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$