heicant - Mathbox for Brendan Leahy

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

Theorem heicant 28452

Description: Heine-Cantor theorem: a continuous mapping between metric spaces whose domain is compact is uniformly continuous. Theorem on [Rosenlicht] p. 80. (Contributed by Brendan Leahy, 13-Aug-2018.)

**Hypotheses**
Ref	Expression
heicant.c
heicant.d
heicant.j
heicant.x
heicant.y

**Assertion**
Ref	Expression
heicant	metUnif Cn_umetUnif

Proof of Theorem heicant Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 4317	. . . . . . . . . . 11
2	1	imbi2d 316	. . . . . . . . . 10
3	2	2ralbidv 2778	. . . . . . . . 9
4	3	rexbidv 2757	. . . . . . . 8
5	4	cbvralv 2968	. . . . . . 7
6		r19.12 2851	. . . . . . . 8
7	6	ralimi 2812	. . . . . . 7
8	5, 7	sylbi 195	. . . . . 6
9		rphalfcl 11036	. . . . . . . . 9
10		breq2 4317	. . . . . . . . . . . . . . . 16
11	10	imbi2d 316	. . . . . . . . . . . . . . 15
12	11	ralbidv 2756	. . . . . . . . . . . . . 14
13	12	rexbidv 2757	. . . . . . . . . . . . 13
14	13	ralbidv 2756	. . . . . . . . . . . 12
15	14	rspcva 3092	. . . . . . . . . . 11 $/\$
16		heicant.j	. . . . . . . . . . . . . . 15
17	16	ad3antrrr 729	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
18		heicant.c	. . . . . . . . . . . . . . . . . . . . . . . 24
19	18	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
20	19	anim1i 568	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
21		rphalfcl 11036	. . . . . . . . . . . . . . . . . . . . . . 23
22	21	rpxrd 11049	. . . . . . . . . . . . . . . . . . . . . 22
23		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . 24
24	23	blopn 20097	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
25	24	3expa 1187	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
26	20, 22, 25	syl2an 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
27	26	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
28	21	rpgt0d 11051	. . . . . . . . . . . . . . . . . . . . . . 23
29	22, 28	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
30		xblcntr 20008	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
31	30	3expa 1187	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
32	20, 29, 31	syl2an 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
33	32	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
34		opelxpi 4892	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
35	21, 34	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
36	35	adantll 713	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
37	36	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
38		rpcn 11020	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
39	38	2halvesd 10591	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
40	39	breq2d 4325	. . . . . . . . . . . . . . . . . . . . . . . . . 26
41	40	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . . . . 25
42	41	ralbidv 2756	. . . . . . . . . . . . . . . . . . . . . . . 24
43		oveq2 6120	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
44	43	breq1d 4323	. . . . . . . . . . . . . . . . . . . . . . . . . 26
45		fveq2 5712	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
46	45	oveq2d 6128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
47	46	breq1d 4323	. . . . . . . . . . . . . . . . . . . . . . . . . 26
48	44, 47	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	48	cbvralv 2968	. . . . . . . . . . . . . . . . . . . . . . . 24
50	42, 49	syl6bb 261	. . . . . . . . . . . . . . . . . . . . . . 23
51	50	biimpar 485	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
52	51	adantll 713	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
53		vex 2996	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
54		ovex 6137	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
55	53, 54	op1std 6608	. . . . . . . . . . . . . . . . . . . . . . . . . 26
56	53, 54	op2ndd 6609	. . . . . . . . . . . . . . . . . . . . . . . . . 26
57	55, 56	oveq12d 6130	. . . . . . . . . . . . . . . . . . . . . . . . 25
58	57	eqcomd 2448	. . . . . . . . . . . . . . . . . . . . . . . 24
59	58	biantrurd 508	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
60	55	oveq1d 6127	. . . . . . . . . . . . . . . . . . . . . . . . . 26
61	56, 56	oveq12d 6130	. . . . . . . . . . . . . . . . . . . . . . . . . 26
62	60, 61	breq12d 4326	. . . . . . . . . . . . . . . . . . . . . . . . 25
63	55	fveq2d 5716	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
64	63	oveq1d 6127	. . . . . . . . . . . . . . . . . . . . . . . . . 26
65	64	breq1d 4323	. . . . . . . . . . . . . . . . . . . . . . . . 25
66	62, 65	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . 24
67	66	ralbidv 2756	. . . . . . . . . . . . . . . . . . . . . . 23
68	59, 67	bitr3d 255	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
69	68	rspcev 3094	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
70	37, 52, 69	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71		eleq2 2504	. . . . . . . . . . . . . . . . . . . . . 22
72		eqeq1 2449	. . . . . . . . . . . . . . . . . . . . . . . 24
73	72	anbi1d 704	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
74	73	rexbidv 2757	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
75	71, 74	anbi12d 710	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
76	75	rspcev 3094	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
77	27, 33, 70, 76	syl12anc 1216	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	ex 434	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79	78	rexlimdva 2862	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
80	79	ralimdva 2815	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
81	80	imp 429	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
82	23	mopnuni 20038	. . . . . . . . . . . . . . . . . 18
83	18, 82	syl 16	. . . . . . . . . . . . . . . . 17
84	83	raleqdv 2944	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
85	84	ad3antrrr 729	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86	81, 85	mpbid 210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
87		eqid 2443	. . . . . . . . . . . . . . 15
88		fveq2 5712	. . . . . . . . . . . . . . . . . 18
89		fveq2 5712	. . . . . . . . . . . . . . . . . 18
90	88, 89	oveq12d 6130	. . . . . . . . . . . . . . . . 17
91	90	eqeq2d 2454	. . . . . . . . . . . . . . . 16
92	88	oveq1d 6127	. . . . . . . . . . . . . . . . . . 19
93	89, 89	oveq12d 6130	. . . . . . . . . . . . . . . . . . 19
94	92, 93	breq12d 4326	. . . . . . . . . . . . . . . . . 18
95	88	fveq2d 5716	. . . . . . . . . . . . . . . . . . . 20
96	95	oveq1d 6127	. . . . . . . . . . . . . . . . . . 19
97	96	breq1d 4323	. . . . . . . . . . . . . . . . . 18
98	94, 97	imbi12d 320	. . . . . . . . . . . . . . . . 17
99	98	ralbidv 2756	. . . . . . . . . . . . . . . 16
100	91, 99	anbi12d 710	. . . . . . . . . . . . . . 15 $/\$ $/\$
101	87, 100	cmpcovf 19016	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	17, 86, 101	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	102	ex 434	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
104		inss2 3592	. . . . . . . . . . . . . . 15
105	104	sseli 3373	. . . . . . . . . . . . . 14
106		simpll 753	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	106	anim1i 568	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
108		frn 5586	. . . . . . . . . . . . . . . . . . . . . . . 24
109		rnss 5089	. . . . . . . . . . . . . . . . . . . . . . . 24
110	108, 109	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23
111		rnxpss 5291	. . . . . . . . . . . . . . . . . . . . . . 23
112	110, 111	syl6ss 3389	. . . . . . . . . . . . . . . . . . . . . 22
113	112	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
114		simplr 754	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
115		ffun 5582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
116		vex 2996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
117	116	fundmen 7404	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
118	117	ensymd 7381	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
119	115, 118	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26
120		fdm 5584	. . . . . . . . . . . . . . . . . . . . . . . . . 26
121	119, 120	breqtrd 4337	. . . . . . . . . . . . . . . . . . . . . . . . 25
122		enfii 7551	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
123	121, 122	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
124		rnfi 7617	. . . . . . . . . . . . . . . . . . . . . . . 24
125		rnfi 7617	. . . . . . . . . . . . . . . . . . . . . . . 24
126	123, 124, 125	3syl 20	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
127	114, 126	sylan 471	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
128	120	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
129		eqtr 2460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
130	83, 129	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
131		heicant.x	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
132	131	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
133	130, 132	eqnetrrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
134		unieq 4120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
135		uni0 4139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
136	134, 135	syl6eq 2491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
137	136	necon3i 2674	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
138	133, 137	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
139	138	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
140	128, 139	eqnetrd 2654	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
141		dm0rn0 5077	. . . . . . . . . . . . . . . . . . . . . . . . . 26
142	141	necon3bii 2634	. . . . . . . . . . . . . . . . . . . . . . . . 25
143	140, 142	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
144		relxp 4968	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
145		relss 4948	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
146	108, 144, 145	mpisyl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26
147		relrn0 5118	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
148	147	necon3bid 2637	. . . . . . . . . . . . . . . . . . . . . . . . . 26
149	146, 148	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25
150	149	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
151	143, 150	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
152	151	adantllr 718	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
153		rpssre 11022	. . . . . . . . . . . . . . . . . . . . . . 23
154	113, 153	syl6ss 3389	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
155		ltso 9476	. . . . . . . . . . . . . . . . . . . . . . . 24
156		cnvso 5397	. . . . . . . . . . . . . . . . . . . . . . . 24
157	155, 156	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . 23
158		fisupcl 7738	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
159	157, 158	mpan 670	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
160	127, 152, 154, 159	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
161	113, 160	sseldd 3378	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
162	107, 161	sylanl1 650	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
163	162	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164	83	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
165	164	anim1i 568	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
166	165	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167		simpl 457	. . . . . . . . . . . . . . . . . . . . 21 $/\$
168	129	eleq2d 2510	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
169		eluni2 4116	. . . . . . . . . . . . . . . . . . . . . . 23
170	168, 169	syl6bb 261	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
171	170	biimpa 484	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
172	166, 167, 171	syl2an 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
173		nfv 1673	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
174		nfra1 2787	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
175	173, 174	nfan 1861	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176		nfv 1673	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
177	175, 176	nfan 1861	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178		nfv 1673	. . . . . . . . . . . . . . . . . . . . 21
179		rsp 2797	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
180	179	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
181		oveq2 6120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
182	181	breq1d 4323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
183		fveq2 5712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
184	183	oveq2d 6128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
185	184	breq1d 4323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
186	182, 185	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
187	186	rspcva 3092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
188		oveq2 6120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
189	188	breq1d 4323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
190	45	oveq2d 6128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
191	190	breq1d 4323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
192	189, 191	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
193	192	rspcva 3092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
194	187, 193	anim12i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
195	194	anandirs 827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
196		prth 571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
197	195, 196	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
198	197	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
199	198	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
200	199	adantlll 717	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
201		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
202	201	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
203	202	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
204	112, 153	syl6ss 3389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
205	204	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
206		0re 9407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
207		rpge0 11024	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
208	207	rgen 2802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
209		ssralv 3437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
210	112, 208, 209	mpisyl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
211		breq1 4316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
212	211	ralbidv 2756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
213	212	rspcev 3094	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
214	206, 210, 213	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
215	214	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
216	146	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
217		ffn 5580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
218		fnfvelrn 5861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
219	217, 218	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
220		2ndrn 6643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
221	216, 219, 220	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
222		infmrlb 10332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
223	205, 215, 221, 222	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
224	223	adantll 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
225	224	ad2ant2r 746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
226	18	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
227		xmetcl 19928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
228	227	3expb 1188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
229	226, 228	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
230	229	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
231		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
232		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
233		ne0i 3664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
234	221, 233	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
235		infmrcl 10330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
236	205, 234, 215, 235	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
237	236	rexrd 9454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
238	231, 232, 237	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
239		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
240	239	ffvelrnda 5864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
241		xp2nd 6628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
242	240, 241	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
243	242	rpxrd 11049	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
244	243	ad2ant2r 746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245		xrltletr 11152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
246	230, 238, 244, 245	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
247	225, 246	mpan2d 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
248	247	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
249	18	ad6antr 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
250		simpllr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
251		ffvelrn 5862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
252		xp1st 6627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
253	251, 252	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
254	250, 232, 253	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$