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 30030

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 30029	. 2 $/\$ $/\$ $/\$
2		elpwi 4006	. . . . 5
3		elmapi 7442	. . . . . . . . . . . 12
4		inss1 3703	. . . . . . . . . . . . . . . . . . . 20
5		ovolsscl 21770	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
6	4, 5	mp3an1 1312	. . . . . . . . . . . . . . . . . . 19 $/\$
7		difss 3616	. . . . . . . . . . . . . . . . . . . 20 $\$
8		ovolsscl 21770	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$
9	7, 8	mp3an1 1312	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
10	6, 9	readdcld 9626	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
11	10	rexrd 9646	. . . . . . . . . . . . . . . . 17 $/\$ $\$
12	11	ad3antlr 730	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
13		rncoss 5253	. . . . . . . . . . . . . . . . . . 19
14	13	unissi 4257	. . . . . . . . . . . . . . . . . 18
15		unirnioo 11633	. . . . . . . . . . . . . . . . . 18
16	14, 15	sseqtr4i 3522	. . . . . . . . . . . . . . . . 17
17		ovolcl 21762	. . . . . . . . . . . . . . . . 17
18	16, 17	mp1i 12	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		eqid 2443	. . . . . . . . . . . . . . . . . . 19
20		eqid 2443	. . . . . . . . . . . . . . . . . . 19
21	19, 20	ovolsf 21757	. . . . . . . . . . . . . . . . . 18
22		frn 5727	. . . . . . . . . . . . . . . . . . 19
23		icossxr 11618	. . . . . . . . . . . . . . . . . . 19
24	22, 23	syl6ss 3501	. . . . . . . . . . . . . . . . . 18
25		supxrcl 11515	. . . . . . . . . . . . . . . . . 18
26	21, 24, 25	3syl 20	. . . . . . . . . . . . . . . . 17
27	26	ad2antlr 726	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		pnfge 11348	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
29	11, 28	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$
30	29	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $\$
31		simpr 461	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
32	30, 31	breqtrrd 4463	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $\$
33	32	adantlll 717	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
34	16, 17	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
35		nltpnft 11376	. . . . . . . . . . . . . . . . . . . . . 22
36	34, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
37	36	necon2abii 2709	. . . . . . . . . . . . . . . . . . . 20
38		ovolge0 21765	. . . . . . . . . . . . . . . . . . . . . 22
39	16, 38	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
40		0re 9599	. . . . . . . . . . . . . . . . . . . . . 22
41		xrre3 11381	. . . . . . . . . . . . . . . . . . . . . 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 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
48		uniretop 21142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
49	48	cldss 19403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
50		dfss4 3717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
51	49, 50	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
52		rembl 21824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
53	48	cldopn 19405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$
54		opnmbl 21884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$
55	53, 54	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
56		difmbl 21826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $\$ $\$ $\$
57	52, 55, 56	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
58	51, 57	eqeltrrd 2532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
59	47, 58	vtoclga 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		mblvol 21814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
61	59, 60	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62	46, 61	sylan9eqr 2506	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
63	62	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
64		inss1 3703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
65		sstr 3497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
66	64, 65	mpan2 671	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	66	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
68		ovolsscl 21770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
69	16, 68	mp3an2 1313	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	69	ancoms 453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
71	67, 70	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
72	63, 71	eqeltrd 2531	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
73	72	rexlimdvaa 2936	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
74	73	abssdv 3559	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
75		eqeq1 2447	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
76	75	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
77	76	rexbidv 2954	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
78	77	ralab 3246	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
79		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
80	79, 61	sylan9eqr 2506	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
81		ovolss 21769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
82	66, 16, 81	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
83	82	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
84	80, 83	eqbrtrd 4457	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
85	84	rexlimiva 2931	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
86	78, 85	mpgbir 1609	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
87		breq2 4441	. . . . . . . . . . . . . . . . . . . . . . . . . 26
88	87	ralbidv 2882	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
89	88	rspcev 3196	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
90	86, 89	mpan2 671	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
91		retop 21141	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
92		0cld 19412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
93	91, 92	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
94		0ss 3800	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
95		0mbl 21823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		mblvol 21814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98		ovol0 21777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	97, 98	eqtr2i 2473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
100	94, 99	pm3.2i 455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
101		sseq1 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102		fveq2 5856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
103	102	eqeq2d 2457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
104	101, 103	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
105	104	rspcev 3196	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
106	93, 100, 105	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
107		c0ex 9593	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
108		eqeq1 2447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
109	108	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
110	109	rexbidv 2954	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
111	107, 110	elab 3232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
112	106, 111	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
113	112	ne0ii 3777	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
114		suprcl 10509	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	113, 114	mp3an2 1313	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
116	74, 90, 115	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
117		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$
118		eleq1 2515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
119	118, 58	vtoclga 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
120		mblvol 21814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	119, 120	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	117, 121	sylan9eqr 2506	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
123	122	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
124		difss2 3618	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
125	124	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
126		ovolsscl 21770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
127	16, 126	mp3an2 1313	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
128	127	ancoms 453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
129	125, 128	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
130	123, 129	eqeltrd 2531	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
131	130	rexlimdvaa 2936	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
132	131	abssdv 3559	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$
133		eqeq1 2447	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
134	133	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
135	134	rexbidv 2954	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
136	135	ralab 3246	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $/\$
137		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$
138	137, 121	sylan9eqr 2506	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
139		ovolss 21769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
140	124, 16, 139	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
141	140	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
142	138, 141	eqbrtrd 4457	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $/\$
143	142	rexlimiva 2931	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
144	136, 143	mpgbir 1609	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
145	87	ralbidv 2882	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $/\$
146	145	rspcev 3196	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $\$ $/\$
147	144, 146	mpan2 671	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$
148		0ss 3800	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
149	148, 99	pm3.2i 455	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$
150		sseq1 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
151		fveq2 5856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
152	151	eqeq2d 2457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
153	150, 152	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
154	153	rspcev 3196	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$ $\$ $/\$
155	93, 149, 154	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$
156		eqeq1 2447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
157	156	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
158	157	rexbidv 2954	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
159	107, 158	elab 3232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
160	155, 159	mpbir 209	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
161	160	ne0ii 3777	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
162		suprcl 10509	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
163	161, 162	mp3an2 1313	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
164	132, 147, 163	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
165	116, 164	readdcld 9626	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$
166	165	adantl 466	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
167		simpr 461	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
168	6	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
169	9	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$
170		ovolsscl 21770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
171	64, 16, 170	mp3an12 1315	. . . . . . . . . . . . . . . . . . . . . . . . 25
172	171	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
173		difss 3616	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
174		ovolsscl 21770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$ $\$
175	173, 16, 174	mp3an12 1315	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
176	175	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$
177		ssrin 3708	. . . . . . . . . . . . . . . . . . . . . . . . . 26
178	64, 16	sstri 3498	. . . . . . . . . . . . . . . . . . . . . . . . . 26
179		ovolss 21769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
180	177, 178, 179	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . 25
181	180	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
182		ssdif 3624	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
183	173, 16	sstri 3498	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
184		ovolss 21769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $/\$ $\$ $\$ $\$
185	182, 183, 184	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
186	185	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$ $\$
187	168, 169, 172, 176, 181, 186	le2addd 10176	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$ $\$
188		dfin4 3723	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
189	188	fveq2i 5859	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
190	189	oveq1i 6291	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$
191	187, 190	syl6breq 4476	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
192	191	adantlll 717	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
193		simpll 753	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
194	188	sseq2i 3514	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
195	194	anbi1i 695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $\$ $/\$
196	195	rexbii 2945	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $\$ $/\$
197	196	abbii 2577	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $\$ $/\$
198	197	supeq1i 7909	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $\$ $/\$
199	16	jctl 541	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
200	199	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
201	175, 183	jctil 537	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$
202	201	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
203		ltso 9668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
204	203	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
205		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
206		vex 3098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
207		eqeq1 2447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
208	207	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
209	208	rexbidv 2954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
210	206, 209	elab 3232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
211	16, 139	mpan2 671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
212	211	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
213	48	cldss 19403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
214		ovolcl 21762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
215	213, 214	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
216		xrlenlt 9655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
217	215, 34, 216	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
218	217	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
219		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
220	219, 121	sylan9eqr 2506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
221		breq2 4441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
222	221	notbid 294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
223	220, 222	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
224	223	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
225	218, 224	bitr4d 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
226	212, 225	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
227	226	rexlimiva 2931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
228	210, 227	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
229	228	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
230		retopbas 21140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
231		bastg 19340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
232	230, 231	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
233	13, 232	sstri 3498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
234		uniopn 19279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
235	91, 233, 234	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
236		mblfinlem2 30027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
237	235, 236	mp3an1 1312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
238	121	eqcomd 2451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
239	238	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
240	239	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
241	240	anim2d 565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
242		fvex 5866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
243		eqeq1 2447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
244	243	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
245		breq2 4441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
246	244, 245	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
247	242, 246	spcev 3187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
248	247	anasss 647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
249	241, 248	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
250	249	reximia 2909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
251	237, 250	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
252		r19.41v 2995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
253	252	exbii 1654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
254		rexcom4 3115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
255	133	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
256	255	rexbidv 2954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
257	256	rexab 3248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
258	253, 254, 257	3bitr4i 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
259	251, 258	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
260	259	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
261	204, 205, 229, 260	eqsupd 7919	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
262	261	eqcomd 2451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
263	262	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
264		sseq1 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
265		fveq2 5856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
266	265	eqeq2d 2457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
267	264, 266	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
268	267	cbvrexv 3071	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
269	268	abbii 2577	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
270	269	supeq1i 7909	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
271	263, 270	syl6eq 2500	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
272		sseq1 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
273	272, 266	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $\$ $/\$
274	273	cbvrexv 3071	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
275	274	abbii 2577	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
276	275	supeq1i 7909	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
277		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
278		eqeq1 2447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
279	278	anbi2d 703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
280	279	rexbidv 2954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
281		sseq1 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
282		fveq2 5856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
283	282	eqeq2d 2457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
284	281, 283	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
285	284	cbvrexv 3071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
286	280, 285	syl6bb 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
287	286	cbvabv 2586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
288	287	supeq1i 7909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
289	288	eqeq2i 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
290	289	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
291	290	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
292		mblfinlem3 30028	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
293	200, 277, 263, 291, 292	syl112anc 1233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$