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 33450

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 33449	. 2 $/\$ $/\$ $/\$
2		elpwi 4168	. . . . 5
3		elmapi 7879	. . . . . . . . . . . 12
4		inss1 3833	. . . . . . . . . . . . . . . . . . . 20
5		ovolsscl 23254	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
6	4, 5	mp3an1 1411	. . . . . . . . . . . . . . . . . . 19 $/\$
7		difss 3737	. . . . . . . . . . . . . . . . . . . 20 $\$
8		ovolsscl 23254	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $\$
9	7, 8	mp3an1 1411	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
10	6, 9	readdcld 10069	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
11	10	rexrd 10089	. . . . . . . . . . . . . . . . 17 $/\$ $\$
12	11	ad3antlr 767	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
13		rncoss 5386	. . . . . . . . . . . . . . . . . . 19
14	13	unissi 4461	. . . . . . . . . . . . . . . . . 18
15		unirnioo 12273	. . . . . . . . . . . . . . . . . 18
16	14, 15	sseqtr4i 3638	. . . . . . . . . . . . . . . . 17
17		ovolcl 23246	. . . . . . . . . . . . . . . . 17
18	16, 17	mp1i 13	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		eqid 2622	. . . . . . . . . . . . . . . . . . 19
20		eqid 2622	. . . . . . . . . . . . . . . . . . 19
21	19, 20	ovolsf 23241	. . . . . . . . . . . . . . . . . 18
22		frn 6053	. . . . . . . . . . . . . . . . . . 19
23		icossxr 12258	. . . . . . . . . . . . . . . . . . 19
24	22, 23	syl6ss 3615	. . . . . . . . . . . . . . . . . 18
25		supxrcl 12145	. . . . . . . . . . . . . . . . . 18
26	21, 24, 25	3syl 18	. . . . . . . . . . . . . . . . 17
27	26	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		pnfge 11964	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
29	11, 28	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$
30	29	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $\$
31		simpr 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
32	30, 31	breqtrrd 4681	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $\$
33	32	adantlll 754	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
34	16, 17	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
35		nltpnft 11995	. . . . . . . . . . . . . . . . . . . . . 22
36	34, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
37	36	necon2abii 2844	. . . . . . . . . . . . . . . . . . . 20
38		ovolge0 23249	. . . . . . . . . . . . . . . . . . . . . 22
39	16, 38	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
40		0re 10040	. . . . . . . . . . . . . . . . . . . . . 22
41		xrre3 12002	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
42	34, 40, 41	mpanl12 718	. . . . . . . . . . . . . . . . . . . . 21 $/\$
43	39, 42	mpan 706	. . . . . . . . . . . . . . . . . . . 20
44	37, 43	sylbir 225	. . . . . . . . . . . . . . . . . . 19
45	10	ad3antlr 767	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
46		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
47		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
48		uniretop 22566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
49	48	cldss 20833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
50		dfss4 3858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$ $\$
51	49, 50	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
52		rembl 23308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
53	48	cldopn 20835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$
54		opnmbl 23370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $\$ $\$
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $\$
56		difmbl 23311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $\$ $\$ $\$
57	52, 55, 56	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $\$
58	51, 57	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
59	47, 58	vtoclga 3272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		mblvol 23298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
61	59, 60	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62	46, 61	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
63	62	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
64		inss1 3833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
65		sstr 3611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
66	64, 65	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
67	66	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
68		ovolsscl 23254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
69	16, 68	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
70	69	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
71	67, 70	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
72	63, 71	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
73	72	rexlimdvaa 3032	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
74	73	abssdv 3676	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
75		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
76	75	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
77	76	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
78	77	ralab 3367	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
79		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
80	79, 61	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
81		ovolss 23253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
82	66, 16, 81	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
83	82	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
84	80, 83	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
85	84	rexlimiva 3028	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
86	78, 85	mpgbir 1726	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
87		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . . . . 26
88	87	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
89	88	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
90	86, 89	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
91		retop 22565	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
92		0cld 20842	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
93	91, 92	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
94		0ss 3972	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
95		0mbl 23307	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
96		mblvol 23298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
98		ovol0 23261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
99	97, 98	eqtr2i 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
100	94, 99	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
101		sseq1 3626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
102		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
103	102	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
104	101, 103	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
105	104	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
106	93, 100, 105	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
107		c0ex 10034	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
108		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
109	108	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
110	109	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
111	107, 110	elab 3350	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
112	106, 111	mpbir 221	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
113	112	ne0ii 3923	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
114		suprcl 10983	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115	113, 114	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
116	74, 90, 115	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
117		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$
118		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
119	118, 58	vtoclga 3272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
120		mblvol 23298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121	119, 120	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
122	117, 121	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
123	122	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
124		difss2 3739	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
125	124	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
126		ovolsscl 23254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
127	16, 126	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
128	127	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
129	125, 128	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
130	123, 129	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$
131	130	rexlimdvaa 3032	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
132	131	abssdv 3676	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$
133		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
134	133	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
135	134	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
136	135	ralab 3367	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $/\$
137		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$
138	137, 121	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
139		ovolss 23253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
140	124, 16, 139	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
141	140	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
142	138, 141	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $/\$
143	142	rexlimiva 3028	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
144	136, 143	mpgbir 1726	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
145	87	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $\$ $/\$
146	145	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $\$ $/\$
147	144, 146	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$
148		0ss 3972	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$
149	148, 99	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$
150		sseq1 3626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $\$
151		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
152	151	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
153	150, 152	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
154	153	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$ $\$ $/\$
155	93, 149, 154	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$
156		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
157	156	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
158	157	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
159	107, 158	elab 3350	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
160	155, 159	mpbir 221	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
161	160	ne0ii 3923	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
162		suprcl 10983	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
163	161, 162	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
164	132, 147, 163	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$
165	116, 164	readdcld 10069	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$
166	165	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
167		simpr 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
168	6	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
169	9	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$
170		ovolsscl 23254	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
171	64, 16, 170	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . . 25
172	171	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
173		difss 3737	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
174		ovolsscl 23254	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$ $\$
175	173, 16, 174	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
176	175	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$
177		ssrin 3838	. . . . . . . . . . . . . . . . . . . . . . . . . 26
178	64, 16	sstri 3612	. . . . . . . . . . . . . . . . . . . . . . . . . 26
179		ovolss 23253	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
180	177, 178, 179	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . 25
181	180	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
182		ssdif 3745	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
183	173, 16	sstri 3612	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$
184		ovolss 23253	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$ $/\$ $\$ $\$ $\$
185	182, 183, 184	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
186	185	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$ $\$
187	168, 169, 172, 176, 181, 186	le2addd 10646	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$ $\$
188		dfin4 3867	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
189	188	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
190	189	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$ $\$
191	187, 190	syl6breq 4694	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
192	191	adantlll 754	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$ $\$ $\$
193		simpll 790	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
194	188	sseq2i 3630	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $\$
195	194	anbi1i 731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $\$ $/\$
196	195	rexbii 3041	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $\$ $/\$
197	196	abbii 2739	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $\$ $/\$
198	197	supeq1i 8353	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $\$ $/\$
199	16	jctl 564	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
200	199	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
201	175, 183	jctil 560	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$
202	201	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
203		ltso 10118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
204	203	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
205		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
206		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
207		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
208	207	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
209	208	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
210	206, 209	elab 3350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
211	16, 139	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
212	211	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
213	48	cldss 20833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
214		ovolcl 23246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
216		xrlenlt 10103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
217	215, 34, 216	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
218	217	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
219		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
220	219, 121	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
221		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
222	221	notbid 308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
223	220, 222	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
224	223	adantrl 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
225	218, 224	bitr4d 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
226	212, 225	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
227	226	rexlimiva 3028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
228	210, 227	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
229	228	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
230		retopbas 22564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
231		bastg 20770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
232	230, 231	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
233	13, 232	sstri 3612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
234		uniopn 20702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
235	91, 233, 234	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
236		mblfinlem2 33447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
237	235, 236	mp3an1 1411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
238	121	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
239	238	anim1i 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
240	239	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
241	240	anim2d 589	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
242		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
243		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
244	243	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
245		breq2 4657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
246	244, 245	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
247	242, 246	spcev 3300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
248	247	anasss 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
249	241, 248	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
250	249	reximia 3009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
251	237, 250	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
252		r19.41v 3089	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
253	252	exbii 1774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
254		rexcom4 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
255	133	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
256	255	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
257	256	rexab 3369	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
258	253, 254, 257	3bitr4i 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
259	251, 258	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
260	259	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
261	204, 205, 229, 260	eqsupd 8363	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
262	261	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
263	262	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$
264		sseq1 3626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
265		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
266	265	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
267	264, 266	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
268	267	cbvrexv 3172	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
269	268	abbii 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
270	269	supeq1i 8353	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
271	263, 270	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$
272		sseq1 3626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $\$
273	272, 266	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $\$ $/\$
274	273	cbvrexv 3172	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$ $\$ $/\$
275	274	abbii 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $\$ $/\$
276	275	supeq1i 8353	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $\$ $/\$
277		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
278		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
279	278	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
280	279	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
281		sseq1 3626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
282		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
283	282	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
284	281, 283	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
285	284	cbvrexv 3172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
286	280, 285	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
287	286	cbvabv 2747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
288	287	supeq1i 8353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
289	288	eqeq2i 2634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
290	289	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
291	290	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$
292		mblfinlem3 33448	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
293	200, 277, 263, 291, 292	syl112anc 1330	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
294	276, 293	syl5reqr 2671	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$
295		mblfinlem3 33448	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$ $/\$ $\$ $\$
296	200, 202, 271, 294, 295	syl112anc 1330	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $\$ $\$ $/\$ $\$ $\$
297	198, 296	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $\$
298	297, 293	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $\$
299	193, 298	sylan 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$ $\$
300	192, 299	breqtrrd 4681	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $/\$
301		ne0i 3921	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
302	112, 301	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
303		ne0i 3921	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$ $\$ $/\$
304	160, 303	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$
305		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$ $\$ $/\$
306	74, 302, 90, 132, 304, 147, 305	supadd 10991	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$ $/\$ $\$ $/\$
307		reeanv 3107	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$
308		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
309		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
310	309	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
311	310	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
312	308, 311	elab 3350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
313		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
314		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
315	314	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $\$ $/\$ $\$ $/\$
316	315	rexbidv 3052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $\$ $/\$ $\$ $/\$
317	313, 316	elab 3350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$ $/\$ $\$ $/\$
318	312, 317	anbi12i 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$
319	307, 318	bitr4i 267	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$
320		an4 865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
321		oveq12 6659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
322	59	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
323	322	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $\$
324	119	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
325	324	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $\$
326		ss2in 3840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $\$ $\$
327	188	ineq1i 3810	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $\$ $\$ $\$ $\$
328		incom 3805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $\$ $\$ $\$ $\$ $\$ $\$
329		disjdif 4040	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $\$ $\$ $\$
330	327, 328, 329	3eqtri 2648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $\$
331	326, 330	syl6sseq 3651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $\$
332		ss0 3974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
333	331, 332	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $\$
334	333	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $\$
335	61	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
336	335	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $\$
337	66, 16	jctir 561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
338	68	3expa 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
339	337, 338	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
340	339	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
341	340	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $\$
342	336, 341	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $\$
343	121	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
344	343	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $\$
345	124, 16	jctir 561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $\$ $/\$
346	126	3expa 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
347	345, 346	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $\$ $/\$
348	347	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $\$
349	348	ad2ant2rl 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $\$
350	344, 349	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $\$
351		volun 23313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
352	323, 325, 334, 342, 350, 351	syl32anc 1334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $\$
353		unmbl 23305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
354	59, 119, 353	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
355		mblvol 23298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
356	354, 355	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
357	356	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $\$
358	352, 357	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $\$
359	321, 358	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
360		eqtr 2641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
361	360	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
362	359, 361	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
363	66, 124	anim12i 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $\$ $/\$
364		unss 3787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
365	363, 364	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $\$
366		ovolss 23253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
367	365, 16, 366	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $\$
368	367	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
369	362, 368	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$
370	369	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$
371	370	expl 648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
372	320, 371	syl5bir 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
373	372	rexlimdvva 3038	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\$ $/\$
374	319, 373	syl5bir 233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$
375	374	rexlimdvv 3037	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$
376	375	alrimiv 1855	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$
377		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . 26
378	377	2rexbidv 3057	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$ $/\$ $\$ $/\$
379	378	ralab 3367	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $/\$ $\$ $/\$
380	376, 379	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$
381		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
382	74	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
383	132	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $\$ $/\$
384		readdcl 10019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
385	382, 383, 384	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
386	385	anandis 873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $\$ $/\$
387	386	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
388	381, 387	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $\$ $/\$ $/\$
389	388	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $\$ $/\$
390	389	rexlimdvva 3038	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $/\$
391	390	abssdv 3676	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$
392		00id 10211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
393	392	eqcomi 2631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
394		rspceov 6692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$
395	112, 160, 393, 394	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$ $/\$
396		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
397	396	2rexbidv 3057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\$ $/\$ $/\$ $\$ $/\$
398	107, 397	spcev 3300	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\$ $/\$ $/\$ $\$ $/\$
399	395, 398	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$
400		abn0 3954	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$ $/\$ $\$ $/\$
401	399, 400	mpbir 221	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\$ $/\$
402	401	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$
403	87	ralbidv 2986	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\$ $/\$ $/\$ $\$ $/\$
404	403	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
405	380, 404	mpdan 702	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ $/\$
406	391, 402, 405	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$
407		suprleub 10989	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $/\$ $\$ $/\$ $/\$ $\$ $/\$
408	406, 407	mpancom 703	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$ $/\$ $\$ $/\$
409	380, 408	mpbird 247	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\$ $/\$
410	306, 409	eqbrtrd 4675	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $/\$
411	410	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$ $/\$
412	45, 166, 167, 300, 411	letrd 10194	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
413	44, 412	sylan2 491	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
414	33, 413	pm2.61dane 2881	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
415	414	adantlr 751	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
416		ssid 3624	. . . . . . . . . . . . . . . . . 18
417	20	ovollb 23247	. . . . . . . . . . . . . . . . . 18 $/\$
418	416, 417	mpan2 707	. . . . . . . . . . . . . . . . 17
419	418	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
420	12, 18, 27, 415, 419	xrletrd 11993	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
421	420	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
422		simpr 477	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
423	421, 422	breqtrrd 4681	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
424	423	expl 648	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
425	3, 424	sylan2 491	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
426	425	rexlimdva 3031	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
427	426	ralrimivw 2967	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
428		eqeq1 2626	. . . . . . . . . . . 12
429	428	anbi2d 740	. . . . . . . . . . 11 $/\$ $/\$
430	429	rexbidv 3052	. . . . . . . . . 10 $/\$ $/\$
431	430	ralrab 3368	. . . . . . . . 9 $/\$ $\$ $/\$ $\$
432	427, 431	sylibr 224	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
433		ssrab2 3687	. . . . . . . . 9 $/\$
434	11	adantl 482	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
435		infxrgelb 12165	. . . . . . . . 9 $/\$ $/\$ $\$ $\$ inf $/\$ $/\$ $\$
436	433, 434, 435	sylancr 695	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ inf $/\$ $/\$ $\$
437	432, 436	mpbird 247	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $\$ inf $/\$
438		eqid 2622	. . . . . . . . 9 $/\$ $/\$
439	438	ovolval 23242	. . . . . . . 8 inf $/\$
440	439	ad2antrl 764	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ inf $/\$
441	437, 440	breqtrrd 4681	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
442	441	expr 643	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\$
443	2, 442	sylan2 491	. . . 4 $/\$ $/\$ $/\$ $/\$ $\$
444	443	ralrimiva 2966	. . 3 $/\$ $/\$ $/\$ $\$
445		ismbl2 23295	. . . . 5 $/\$ $\$
446	445	baibr 945	. . . 4 $\$
447	446	ad2antrr 762	. . 3 $/\$ $/\$ $/\$ $\$
448	444, 447	mpbid 222	. 2 $/\$ $/\$ $/\$
449	1, 448	impbida 877	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wal 1481

wceq 1483

wex 1704

wcel 1990

cab 2608

wne 2794

wral 2912

wrex 2913

crab 2916 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cpw 4158

cuni 4436 class class class wbr 4653

wor 5034

cxp 5112

cdm 5114

crn 5115

ccom 5118

wf 5884

cfv 5888 (class class class)co 6650

cmap 7857

csup 8346 infcinf 8347

cr 9935

cc0 9936

c1 9937

caddc 9939

cpnf 10071

cxr 10073

clt 10074

cle 10075

cmin 10266

cn 11020

cioo 12175

cico 12177

cseq 12801

cabs 13974

ctg 16098

ctop 20698

ctb 20749

ccld 20820

covol 23231

cvol 23232

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-omul 7565 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-acn 8768 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-rlim 14220 df-sum 14417 df-rest 16083 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750 df-cld 20823 df-cmp 21190 df-conn 21215 df-ovol 23233 df-vol 23234

This theorem is referenced by: (None)

W3C validator