ismblfin - Mathbox for Brendan Leahy

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

Theorem ismblfin 31983

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 31982	. 2 $/\$ $/\$ $/\$
2		elpwi 3928	. . . . 5
3		elmapi 7480	. . . . . . . . . . . 12
4		inss1 3620	. . . . . . . . . . . . . . . . . . . 20
5		ovolsscl 22450	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
6	4, 5	mp3an1 1355	. . . . . . . . . . . . . . . . . . 19 $/\$
7		difss 3528	. . . . . . . . . . . . . . . . . . . 20 $\$
8		ovolsscl 22450	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$
9	7, 8	mp3an1 1355	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
10	6, 9	readdcld 9657	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
11	10	rexrd 9677	. . . . . . . . . . . . . . . . 17 $/\$ $\$
12	11	ad3antlr 742	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
13		rncoss 5073	. . . . . . . . . . . . . . . . . . 19
14	13	unissi 4191	. . . . . . . . . . . . . . . . . 18
15		unirnioo 11724	. . . . . . . . . . . . . . . . . 18
16	14, 15	sseqtr4i 3433	. . . . . . . . . . . . . . . . 17
17		ovolcl 22442	. . . . . . . . . . . . . . . . 17
18	16, 17	mp1i 13	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		eqid 2452	. . . . . . . . . . . . . . . . . . 19
20		eqid 2452	. . . . . . . . . . . . . . . . . . 19
21	19, 20	ovolsf 22436	. . . . . . . . . . . . . . . . . 18
22		frn 5718	. . . . . . . . . . . . . . . . . . 19
23		icossxr 11709	. . . . . . . . . . . . . . . . . . 19
24	22, 23	syl6ss 3412	. . . . . . . . . . . . . . . . . 18
25		supxrcl 11590	. . . . . . . . . . . . . . . . . 18
26	21, 24, 25	3syl 18	. . . . . . . . . . . . . . . . 17
27	26	ad2antlr 738	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		pnfge 11422	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
29	11, 28	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$
30	29	ad2antrr 737	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $\$
31		simpr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
32	30, 31	breqtrrd 4401	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $\$
33	32	adantlll 729	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
34	16, 17	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
35		nltpnft 11451	. . . . . . . . . . . . . . . . . . . . . 22
36	34, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
37	36	necon2abii 2674	. . . . . . . . . . . . . . . . . . . 20
38		ovolge0 22445	. . . . . . . . . . . . . . . . . . . . . 22
39	16, 38	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
40		0re 9630	. . . . . . . . . . . . . . . . . . . . . 22
41		xrre3 11456	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
42	34, 40, 41	mpanl12 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$
43	39, 42	mpan 681	. . . . . . . . . . . . . . . . . . . 20
44	37, 43	sylbir 218	. . . . . . . . . . . . . . . . . . 19
45	10	ad3antlr 742	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
46		simpr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
47		eleq1 2518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
48		uniretop 21794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
49	48	cldss 20055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
50		dfss4 3645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
51	49, 50	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
52		rembl 22505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
53	48	cldopn 20057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$
54		opnmbl 22572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
56		difmbl 22508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $\$ $\$ $\$
57	52, 55, 56	sylancr 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
58	51, 57	eqeltrrd 2531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
59	47, 58	vtoclga 3081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		mblvol 22495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
61	59, 60	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62	46, 61	sylan9eqr 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
63	62	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
64		inss1 3620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
65		sstr 3408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
66	64, 65	mpan2 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	66	ad2antrl 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
68		ovolsscl 22450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
69	16, 68	mp3an2 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	69	ancoms 459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
71	67, 70	sylan2 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
72	63, 71	eqeltrd 2530	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
73	72	rexlimdvaa 2853	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
74	73	abssdv 3471	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
75		eqeq1 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
76	75	anbi2d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
77	76	rexbidv 2873	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
78	77	ralab 3167	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
79		simpr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
80	79, 61	sylan9eqr 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
81		ovolss 22449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
82	66, 16, 81	sylancl 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
83	82	ad2antrl 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
84	80, 83	eqbrtrd 4395	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
85	84	rexlimiva 2849	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
86	78, 85	mpgbir 1677	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
87		breq2 4378	. . . . . . . . . . . . . . . . . . . . . . . . . 26
88	87	ralbidv 2810	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
89	88	rspcev 3118	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
90	86, 89	mpan2 682	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
91		retop 21793	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
92		0cld 20064	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
93	91, 92	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
94		0ss 3731	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
95		0mbl 22504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		mblvol 22495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98		ovol0 22457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	97, 98	eqtr2i 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
100	94, 99	pm3.2i 461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
101		sseq1 3421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
103	102	eqeq2d 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
104	101, 103	anbi12d 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
105	104	rspcev 3118	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
106	93, 100, 105	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
107		c0ex 9624	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
108		eqeq1 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
109	108	anbi2d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
110	109	rexbidv 2873	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
111	107, 110	elab 3153	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
112	106, 111	mpbir 214	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
113	112	ne0ii 3706	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
114		suprcl 10558	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	113, 114	mp3an2 1356	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
116	74, 90, 115	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
117		simpr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$
118		eleq1 2518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
119	118, 58	vtoclga 3081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
120		mblvol 22495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	119, 120	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	117, 121	sylan9eqr 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
123	122	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
124		difss2 3530	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
125	124	ad2antrl 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
126		ovolsscl 22450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
127	16, 126	mp3an2 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
128	127	ancoms 459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
129	125, 128	sylan2 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
130	123, 129	eqeltrd 2530	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
131	130	rexlimdvaa 2853	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
132	131	abssdv 3471	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$
133		eqeq1 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
134	133	anbi2d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
135	134	rexbidv 2873	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
136	135	ralab 3167	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $/\$
137		simpr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$
138	137, 121	sylan9eqr 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
139		ovolss 22449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
140	124, 16, 139	sylancl 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
141	140	ad2antrl 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
142	138, 141	eqbrtrd 4395	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $/\$
143	142	rexlimiva 2849	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
144	136, 143	mpgbir 1677	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
145	87	ralbidv 2810	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $/\$
146	145	rspcev 3118	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $\$ $/\$
147	144, 146	mpan2 682	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$
148		0ss 3731	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
149	148, 99	pm3.2i 461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$
150		sseq1 3421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
151		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
152	151	eqeq2d 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
153	150, 152	anbi12d 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
154	153	rspcev 3118	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$ $\$ $/\$
155	93, 149, 154	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$
156		eqeq1 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
157	156	anbi2d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
158	157	rexbidv 2873	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
159	107, 158	elab 3153	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
160	155, 159	mpbir 214	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
161	160	ne0ii 3706	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
162		suprcl 10558	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
163	161, 162	mp3an2 1356	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
164	132, 147, 163	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
165	116, 164	readdcld 9657	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$
166	165	adantl 472	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
167		simpr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
168	6	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
169	9	ad2antrr 737	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$
170		ovolsscl 22450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
171	64, 16, 170	mp3an12 1358	. . . . . . . . . . . . . . . . . . . . . . . . 25
172	171	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
173		difss 3528	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
174		ovolsscl 22450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$ $\$
175	173, 16, 174	mp3an12 1358	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
176	175	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$
177		ssrin 3625	. . . . . . . . . . . . . . . . . . . . . . . . . 26
178	64, 16	sstri 3409	. . . . . . . . . . . . . . . . . . . . . . . . . 26
179		ovolss 22449	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
180	177, 178, 179	sylancl 673	. . . . . . . . . . . . . . . . . . . . . . . . 25
181	180	ad2antlr 738	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
182		ssdif 3536	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
183	173, 16	sstri 3409	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
184		ovolss 22449	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $/\$ $\$ $\$ $\$
185	182, 183, 184	sylancl 673	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
186	185	ad2antlr 738	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$ $\$
187	168, 169, 172, 176, 181, 186	le2addd 10221	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$ $\$
188		dfin4 3651	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
189	188	fveq2i 5851	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
190	189	oveq1i 6286	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$
191	187, 190	syl6breq 4414	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
192	191	adantlll 729	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
193		simpll 765	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
194	188	sseq2i 3425	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
195	194	anbi1i 706	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $\$ $/\$
196	195	rexbii 2862	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $\$ $/\$
197	196	abbii 2568	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $\$ $/\$
198	197	supeq1i 7948	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $\$ $/\$
199	16	jctl 548	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
200	199	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
201	175, 183	jctil 544	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$
202	201	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
203		ltso 9701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
204	203	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
205		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
206		vex 3016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
207		eqeq1 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
208	207	anbi2d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
209	208	rexbidv 2873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
210	206, 209	elab 3153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
211	16, 139	mpan2 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
212	211	ad2antrl 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
213	48	cldss 20055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
214		ovolcl 22442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
216		xrlenlt 9686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
217	215, 34, 216	sylancl 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
218	217	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
219		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
220	219, 121	sylan9eqr 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
221		breq2 4378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
222	221	notbid 300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
223	220, 222	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
224	223	adantrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
225	218, 224	bitr4d 264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
226	212, 225	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
227	226	rexlimiva 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
228	210, 227	sylbi 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
229	228	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
230		retopbas 21792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
231		bastg 19992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
232	230, 231	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
233	13, 232	sstri 3409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
234		uniopn 19938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
235	91, 233, 234	mp2an 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
236		mblfinlem2 31980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
237	235, 236	mp3an1 1355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
238	121	eqcomd 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
239	238	anim1i 576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
240	239	ex 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
241	240	anim2d 573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
242		fvex 5858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
243		eqeq1 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
244	243	anbi2d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
245		breq2 4378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
246	244, 245	anbi12d 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
247	242, 246	spcev 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
248	247	anasss 657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
249	241, 248	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
250	249	reximia 2831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
251	237, 250	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
252		r19.41v 2910	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
253	252	exbii 1722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
254		rexcom4 3035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
255	133	anbi2d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
256	255	rexbidv 2873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
257	256	rexab 3169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
258	253, 254, 257	3bitr4i 285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
259	251, 258	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
260	259	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
261	204, 205, 229, 260	eqsupd 7958	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
262	261	eqcomd 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
263	262	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
264		sseq1 3421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
265		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
266	265	eqeq2d 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
267	264, 266	anbi12d 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
268	267	cbvrexv 2988	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
269	268	abbii 2568	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
270	269	supeq1i 7948	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
271	263, 270	syl6eq 2502	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
272		sseq1 3421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
273	272, 266	anbi12d 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $\$ $/\$
274	273	cbvrexv 2988	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
275	274	abbii 2568	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
276	275	supeq1i 7948	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
277		simpll 765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
278		eqeq1 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
279	278	anbi2d 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
280	279	rexbidv 2873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
281		sseq1 3421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
282		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
283	282	eqeq2d 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
284	281, 283	anbi12d 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
285	284	cbvrexv 2988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
286	280, 285	syl6bb 269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
287	286	cbvabv 2576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
288	287	supeq1i 7948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
289	288	eqeq2i 2464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
290	289	biimpi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
291	290	ad2antlr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
292		mblfinlem3 31981	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
293	200, 277, 263, 291, 292	syl112anc 1275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$