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 30295

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 30294	. 2 $/\$ $/\$ $/\$
2		elpwi 4008	. . . . 5
3		elmapi 7433	. . . . . . . . . . . 12
4		inss1 3704	. . . . . . . . . . . . . . . . . . . 20
5		ovolsscl 22063	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
6	4, 5	mp3an1 1309	. . . . . . . . . . . . . . . . . . 19 $/\$
7		difss 3617	. . . . . . . . . . . . . . . . . . . 20 $\$
8		ovolsscl 22063	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$
9	7, 8	mp3an1 1309	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
10	6, 9	readdcld 9612	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
11	10	rexrd 9632	. . . . . . . . . . . . . . . . 17 $/\$ $\$
12	11	ad3antlr 728	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
13		rncoss 5252	. . . . . . . . . . . . . . . . . . 19
14	13	unissi 4258	. . . . . . . . . . . . . . . . . 18
15		unirnioo 11627	. . . . . . . . . . . . . . . . . 18
16	14, 15	sseqtr4i 3522	. . . . . . . . . . . . . . . . 17
17		ovolcl 22055	. . . . . . . . . . . . . . . . 17
18	16, 17	mp1i 12	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		eqid 2454	. . . . . . . . . . . . . . . . . . 19
20		eqid 2454	. . . . . . . . . . . . . . . . . . 19
21	19, 20	ovolsf 22050	. . . . . . . . . . . . . . . . . 18
22		frn 5719	. . . . . . . . . . . . . . . . . . 19
23		icossxr 11612	. . . . . . . . . . . . . . . . . . 19
24	22, 23	syl6ss 3501	. . . . . . . . . . . . . . . . . 18
25		supxrcl 11509	. . . . . . . . . . . . . . . . . 18
26	21, 24, 25	3syl 20	. . . . . . . . . . . . . . . . 17
27	26	ad2antlr 724	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		pnfge 11342	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
29	11, 28	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$
30	29	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $\$
31		simpr 459	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
32	30, 31	breqtrrd 4465	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $\$
33	32	adantlll 715	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
34	16, 17	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
35		nltpnft 11370	. . . . . . . . . . . . . . . . . . . . . 22
36	34, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
37	36	necon2abii 2720	. . . . . . . . . . . . . . . . . . . 20
38		ovolge0 22058	. . . . . . . . . . . . . . . . . . . . . 22
39	16, 38	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
40		0re 9585	. . . . . . . . . . . . . . . . . . . . . 22
41		xrre3 11375	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
42	34, 40, 41	mpanl12 680	. . . . . . . . . . . . . . . . . . . . 21 $/\$
43	39, 42	mpan 668	. . . . . . . . . . . . . . . . . . . 20
44	37, 43	sylbir 213	. . . . . . . . . . . . . . . . . . 19
45	10	ad3antlr 728	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
46		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
47		eleq1 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
48		uniretop 21435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
49	48	cldss 19697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
50		dfss4 3729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
51	49, 50	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
52		rembl 22117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
53	48	cldopn 19699	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$
54		opnmbl 22177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$
55	53, 54	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
56		difmbl 22119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $\$ $\$ $\$
57	52, 55, 56	sylancr 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
58	51, 57	eqeltrrd 2543	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
59	47, 58	vtoclga 3170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		mblvol 22107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
61	59, 60	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62	46, 61	sylan9eqr 2517	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
63	62	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
64		inss1 3704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
65		sstr 3497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
66	64, 65	mpan2 669	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	66	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
68		ovolsscl 22063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
69	16, 68	mp3an2 1310	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	69	ancoms 451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
71	67, 70	sylan2 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
72	63, 71	eqeltrd 2542	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
73	72	rexlimdvaa 2947	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
74	73	abssdv 3560	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
75		eqeq1 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
76	75	anbi2d 701	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
77	76	rexbidv 2965	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
78	77	ralab 3257	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
79		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
80	79, 61	sylan9eqr 2517	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
81		ovolss 22062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
82	66, 16, 81	sylancl 660	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
83	82	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
84	80, 83	eqbrtrd 4459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
85	84	rexlimiva 2942	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
86	78, 85	mpgbir 1627	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
87		breq2 4443	. . . . . . . . . . . . . . . . . . . . . . . . . 26
88	87	ralbidv 2893	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
89	88	rspcev 3207	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
90	86, 89	mpan2 669	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
91		retop 21434	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
92		0cld 19706	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
93	91, 92	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
94		0ss 3813	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
95		0mbl 22116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		mblvol 22107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98		ovol0 22070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	97, 98	eqtr2i 2484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
100	94, 99	pm3.2i 453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
101		sseq1 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
103	102	eqeq2d 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
104	101, 103	anbi12d 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
105	104	rspcev 3207	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
106	93, 100, 105	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
107		c0ex 9579	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
108		eqeq1 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
109	108	anbi2d 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
110	109	rexbidv 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
111	107, 110	elab 3243	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
112	106, 111	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
113	112	ne0ii 3790	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
114		suprcl 10498	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	113, 114	mp3an2 1310	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
116	74, 90, 115	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
117		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$
118		eleq1 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
119	118, 58	vtoclga 3170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
120		mblvol 22107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	119, 120	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	117, 121	sylan9eqr 2517	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
123	122	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
124		difss2 3619	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
125	124	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
126		ovolsscl 22063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
127	16, 126	mp3an2 1310	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
128	127	ancoms 451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
129	125, 128	sylan2 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
130	123, 129	eqeltrd 2542	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
131	130	rexlimdvaa 2947	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
132	131	abssdv 3560	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$
133		eqeq1 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
134	133	anbi2d 701	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
135	134	rexbidv 2965	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
136	135	ralab 3257	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $/\$
137		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$
138	137, 121	sylan9eqr 2517	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
139		ovolss 22062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
140	124, 16, 139	sylancl 660	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
141	140	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
142	138, 141	eqbrtrd 4459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $/\$
143	142	rexlimiva 2942	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
144	136, 143	mpgbir 1627	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
145	87	ralbidv 2893	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $/\$
146	145	rspcev 3207	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $\$ $/\$
147	144, 146	mpan2 669	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$
148		0ss 3813	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
149	148, 99	pm3.2i 453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$
150		sseq1 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
151		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
152	151	eqeq2d 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
153	150, 152	anbi12d 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
154	153	rspcev 3207	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$ $\$ $/\$
155	93, 149, 154	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$
156		eqeq1 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
157	156	anbi2d 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
158	157	rexbidv 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
159	107, 158	elab 3243	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
160	155, 159	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
161	160	ne0ii 3790	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
162		suprcl 10498	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
163	161, 162	mp3an2 1310	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
164	132, 147, 163	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
165	116, 164	readdcld 9612	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$
166	165	adantl 464	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
167		simpr 459	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
168	6	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
169	9	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$
170		ovolsscl 22063	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
171	64, 16, 170	mp3an12 1312	. . . . . . . . . . . . . . . . . . . . . . . . 25
172	171	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
173		difss 3617	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
174		ovolsscl 22063	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$ $\$
175	173, 16, 174	mp3an12 1312	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
176	175	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$
177		ssrin 3709	. . . . . . . . . . . . . . . . . . . . . . . . . 26
178	64, 16	sstri 3498	. . . . . . . . . . . . . . . . . . . . . . . . . 26
179		ovolss 22062	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
180	177, 178, 179	sylancl 660	. . . . . . . . . . . . . . . . . . . . . . . . 25
181	180	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
182		ssdif 3625	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
183	173, 16	sstri 3498	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
184		ovolss 22062	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $/\$ $\$ $\$ $\$
185	182, 183, 184	sylancl 660	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
186	185	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$ $\$
187	168, 169, 172, 176, 181, 186	le2addd 10166	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$ $\$
188		dfin4 3735	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
189	188	fveq2i 5851	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
190	189	oveq1i 6280	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$
191	187, 190	syl6breq 4478	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
192	191	adantlll 715	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
193		simpll 751	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
194	188	sseq2i 3514	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
195	194	anbi1i 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $\$ $/\$
196	195	rexbii 2956	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $\$ $/\$
197	196	abbii 2588	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $\$ $/\$
198	197	supeq1i 7898	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $\$ $/\$
199	16	jctl 539	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
200	199	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
201	175, 183	jctil 535	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$
202	201	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
203		ltso 9654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
204	203	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
205		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
206		vex 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
207		eqeq1 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
208	207	anbi2d 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
209	208	rexbidv 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
210	206, 209	elab 3243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
211	16, 139	mpan2 669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
212	211	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
213	48	cldss 19697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
214		ovolcl 22055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
215	213, 214	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
216		xrlenlt 9641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
217	215, 34, 216	sylancl 660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
218	217	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
219		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
220	219, 121	sylan9eqr 2517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
221		breq2 4443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
222	221	notbid 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
223	220, 222	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
224	223	adantrl 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
225	218, 224	bitr4d 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
226	212, 225	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
227	226	rexlimiva 2942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
228	210, 227	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
229	228	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
230		retopbas 21433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
231		bastg 19634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
232	230, 231	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
233	13, 232	sstri 3498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
234		uniopn 19573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
235	91, 233, 234	mp2an 670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
236		mblfinlem2 30292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
237	235, 236	mp3an1 1309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
238	121	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
239	238	anim1i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
240	239	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
241	240	anim2d 563	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
242		fvex 5858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
243		eqeq1 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
244	243	anbi2d 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
245		breq2 4443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
246	244, 245	anbi12d 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
247	242, 246	spcev 3198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
248	247	anasss 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
249	241, 248	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
250	249	reximia 2920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
251	237, 250	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
252		r19.41v 3006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
253	252	exbii 1672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
254		rexcom4 3126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
255	133	anbi2d 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
256	255	rexbidv 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
257	256	rexab 3259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
258	253, 254, 257	3bitr4i 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
259	251, 258	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
260	259	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
261	204, 205, 229, 260	eqsupd 7908	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
262	261	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
263	262	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
264		sseq1 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
265		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
266	265	eqeq2d 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
267	264, 266	anbi12d 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
268	267	cbvrexv 3082	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
269	268	abbii 2588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
270	269	supeq1i 7898	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
271	263, 270	syl6eq 2511	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
272		sseq1 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
273	272, 266	anbi12d 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $\$ $/\$
274	273	cbvrexv 3082	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
275	274	abbii 2588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
276	275	supeq1i 7898	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
277		simpll 751	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
278		eqeq1 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
279	278	anbi2d 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
280	279	rexbidv 2965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
281		sseq1 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
282		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
283	282	eqeq2d 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
284	281, 283	anbi12d 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
285	284	cbvrexv 3082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
286	280, 285	syl6bb 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
287	286	cbvabv 2597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
288	287	supeq1i 7898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
289	288	eqeq2i 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
290	289	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
291	290	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
292		mblfinlem3 30293	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
293	200, 277, 263, 291, 292	syl112anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$