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 31421

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 4399	. . . . . . . . . . 11
2	1	imbi2d 314	. . . . . . . . . 10
3	2	2ralbidv 2848	. . . . . . . . 9
4	3	rexbidv 2918	. . . . . . . 8
5	4	cbvralv 3034	. . . . . . 7
6		r19.12 2933	. . . . . . . 8
7	6	ralimi 2797	. . . . . . 7
8	5, 7	sylbi 195	. . . . . 6
9		rphalfcl 11290	. . . . . . . . 9
10		breq2 4399	. . . . . . . . . . . . . . . 16
11	10	imbi2d 314	. . . . . . . . . . . . . . 15
12	11	ralbidv 2843	. . . . . . . . . . . . . 14
13	12	rexbidv 2918	. . . . . . . . . . . . 13
14	13	ralbidv 2843	. . . . . . . . . . . 12
15	14	rspcva 3158	. . . . . . . . . . 11 $/\$
16		heicant.j	. . . . . . . . . . . . . . 15
17	16	ad3antrrr 728	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
18		heicant.c	. . . . . . . . . . . . . . . . . . . . . . . 24
19	18	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
20	19	anim1i 566	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
21		rphalfcl 11290	. . . . . . . . . . . . . . . . . . . . . . 23
22	21	rpxrd 11305	. . . . . . . . . . . . . . . . . . . . . 22
23		eqid 2402	. . . . . . . . . . . . . . . . . . . . . . . 24
24	23	blopn 21295	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
25	24	3expa 1197	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
26	20, 22, 25	syl2an 475	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
27	26	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
28	21	rpgt0d 11307	. . . . . . . . . . . . . . . . . . . . . . 23
29	22, 28	jca 530	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
30		xblcntr 21206	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
31	30	3expa 1197	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
32	20, 29, 31	syl2an 475	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
33	32	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
34		opelxpi 4855	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
35	21, 34	sylan2 472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
36	35	adantll 712	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
37	36	adantr 463	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
38		rpcn 11273	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
39	38	2halvesd 10825	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
40	39	breq2d 4407	. . . . . . . . . . . . . . . . . . . . . . . . . 26
41	40	imbi1d 315	. . . . . . . . . . . . . . . . . . . . . . . . 25
42	41	ralbidv 2843	. . . . . . . . . . . . . . . . . . . . . . . 24
43		oveq2 6286	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
44	43	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . 26
45		fveq2 5849	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
46	45	oveq2d 6294	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
47	46	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . 26
48	44, 47	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	48	cbvralv 3034	. . . . . . . . . . . . . . . . . . . . . . . 24
50	42, 49	syl6bb 261	. . . . . . . . . . . . . . . . . . . . . . 23
51	50	biimpar 483	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
52	51	adantll 712	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
53		vex 3062	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
54		ovex 6306	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
55	53, 54	op1std 6794	. . . . . . . . . . . . . . . . . . . . . . . . . 26
56	53, 54	op2ndd 6795	. . . . . . . . . . . . . . . . . . . . . . . . . 26
57	55, 56	oveq12d 6296	. . . . . . . . . . . . . . . . . . . . . . . . 25
58	57	eqcomd 2410	. . . . . . . . . . . . . . . . . . . . . . . 24
59	58	biantrurd 506	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
60	55	oveq1d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . 26
61	56, 56	oveq12d 6296	. . . . . . . . . . . . . . . . . . . . . . . . . 26
62	60, 61	breq12d 4408	. . . . . . . . . . . . . . . . . . . . . . . . 25
63	55	fveq2d 5853	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
64	63	oveq1d 6293	. . . . . . . . . . . . . . . . . . . . . . . . . 26
65	64	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . 25
66	62, 65	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . 24
67	66	ralbidv 2843	. . . . . . . . . . . . . . . . . . . . . . 23
68	59, 67	bitr3d 255	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
69	68	rspcev 3160	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
70	37, 52, 69	syl2anc 659	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71		eleq2 2475	. . . . . . . . . . . . . . . . . . . . . 22
72		eqeq1 2406	. . . . . . . . . . . . . . . . . . . . . . . 24
73	72	anbi1d 703	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
74	73	rexbidv 2918	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
75	71, 74	anbi12d 709	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
76	75	rspcev 3160	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
77	27, 33, 70, 76	syl12anc 1228	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	ex 432	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79	78	rexlimdva 2896	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
80	79	ralimdva 2812	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
81	80	imp 427	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
82	23	mopnuni 21236	. . . . . . . . . . . . . . . . . 18
83	18, 82	syl 17	. . . . . . . . . . . . . . . . 17
84	83	raleqdv 3010	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
85	84	ad3antrrr 728	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86	81, 85	mpbid 210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
87		eqid 2402	. . . . . . . . . . . . . . 15
88		fveq2 5849	. . . . . . . . . . . . . . . . . 18
89		fveq2 5849	. . . . . . . . . . . . . . . . . 18
90	88, 89	oveq12d 6296	. . . . . . . . . . . . . . . . 17
91	90	eqeq2d 2416	. . . . . . . . . . . . . . . 16
92	88	oveq1d 6293	. . . . . . . . . . . . . . . . . . 19
93	89, 89	oveq12d 6296	. . . . . . . . . . . . . . . . . . 19
94	92, 93	breq12d 4408	. . . . . . . . . . . . . . . . . 18
95	88	fveq2d 5853	. . . . . . . . . . . . . . . . . . . 20
96	95	oveq1d 6293	. . . . . . . . . . . . . . . . . . 19
97	96	breq1d 4405	. . . . . . . . . . . . . . . . . 18
98	94, 97	imbi12d 318	. . . . . . . . . . . . . . . . 17
99	98	ralbidv 2843	. . . . . . . . . . . . . . . 16
100	91, 99	anbi12d 709	. . . . . . . . . . . . . . 15 $/\$ $/\$
101	87, 100	cmpcovf 20184	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	17, 86, 101	syl2anc 659	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	102	ex 432	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
104		inss2 3660	. . . . . . . . . . . . . . 15
105	104	sseli 3438	. . . . . . . . . . . . . 14
106		simpll 752	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	106	anim1i 566	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
108		frn 5720	. . . . . . . . . . . . . . . . . . . . . . . 24
109		rnss 5052	. . . . . . . . . . . . . . . . . . . . . . . 24
110	108, 109	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
111		rnxpss 5257	. . . . . . . . . . . . . . . . . . . . . . 23
112	110, 111	syl6ss 3454	. . . . . . . . . . . . . . . . . . . . . 22
113	112	adantl 464	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
114		simplr 754	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
115		ffun 5716	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
116		vex 3062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
117	116	fundmen 7627	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
118	117	ensymd 7604	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
119	115, 118	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
120		fdm 5718	. . . . . . . . . . . . . . . . . . . . . . . . . 26
121	119, 120	breqtrd 4419	. . . . . . . . . . . . . . . . . . . . . . . . 25
122		enfii 7772	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
123	121, 122	sylan2 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
124		rnfi 7839	. . . . . . . . . . . . . . . . . . . . . . . 24
125		rnfi 7839	. . . . . . . . . . . . . . . . . . . . . . . 24
126	123, 124, 125	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
127	114, 126	sylan 469	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
128	120	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
129		eqtr 2428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
130	83, 129	sylan 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
131		heicant.x	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
132	131	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
133	130, 132	eqnetrrd 2697	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
134		unieq 4199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
135		uni0 4218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
136	134, 135	syl6eq 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
137	136	necon3i 2643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
138	133, 137	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
139	138	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
140	128, 139	eqnetrd 2696	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
141		dm0rn0 5040	. . . . . . . . . . . . . . . . . . . . . . . . . 26
142	141	necon3bii 2671	. . . . . . . . . . . . . . . . . . . . . . . . 25
143	140, 142	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
144		relxp 4931	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
145		relss 4911	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
146	108, 144, 145	mpisyl 21	. . . . . . . . . . . . . . . . . . . . . . . . . 26
147		relrn0 5081	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
148	147	necon3bid 2661	. . . . . . . . . . . . . . . . . . . . . . . . . 26
149	146, 148	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
150	149	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
151	143, 150	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
152	151	adantllr 717	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
153		rpssre 11275	. . . . . . . . . . . . . . . . . . . . . . 23
154	113, 153	syl6ss 3454	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
155		gtso 9697	. . . . . . . . . . . . . . . . . . . . . . 23
156		fisupcl 7961	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
157	155, 156	mpan 668	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
158	127, 152, 154, 157	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
159	113, 158	sseldd 3443	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
160	107, 159	sylanl1 648	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
161	160	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	83	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
163	162	anim1i 566	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
164	163	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
165		simpl 455	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	129	eleq2d 2472	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
167		eluni2 4195	. . . . . . . . . . . . . . . . . . . . . . 23
168	166, 167	syl6bb 261	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
169	168	biimpa 482	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
170	164, 165, 169	syl2an 475	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
171		nfv 1728	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
172		nfra1 2785	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
173	171, 172	nfan 1956	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174		nfv 1728	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
175	173, 174	nfan 1956	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176		nfv 1728	. . . . . . . . . . . . . . . . . . . . 21
177		rspa 2771	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
178		oveq2 6286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
179	178	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
180		fveq2 5849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
181	180	oveq2d 6294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
182	181	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
183	179, 182	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
184	183	rspcva 3158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
185		oveq2 6286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
186	185	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
187	45	oveq2d 6294	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
188	187	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
189	186, 188	imbi12d 318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
190	189	rspcva 3158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
191	184, 190	anim12i 564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
192	191	anandirs 832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
193		prth 569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
194	192, 193	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
195	194	adantrl 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
196	195	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
197	196	adantlll 716	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
198		simpll 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
199	198	anim1i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
200	199	anim1i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
201	112, 153	syl6ss 3454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
202	201	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
203		0re 9626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
204		rpge0 11277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
205	204	rgen 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
206		ssralv 3503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
207	112, 205, 206	mpisyl 21	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
208		breq1 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
209	208	ralbidv 2843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
210	209	rspcev 3160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
211	203, 207, 210	sylancr 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
212	211	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
213	146	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
214		ffn 5714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
215		fnfvelrn 6006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
216	214, 215	sylan 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
217		2ndrn 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
218	213, 216, 217	syl2anc 659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
219		infmrlb 10564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
220	202, 212, 218, 219	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
221	220	adantll 712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
222	221	ad2ant2r 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
223	18	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
224		xmetcl 21126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
225	224	3expb 1198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
226	223, 225	sylan 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
227	226	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
228		simplr 754	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
229		simpl 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
230		ne0i 3744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
231	218, 230	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
232		infmrcl 10562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
233	202, 231, 212, 232	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
234	233	rexrd 9673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
235	228, 229, 234	syl2an 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
236		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
237	236	ffvelrnda 6009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
238		xp2nd 6815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
239	237, 238	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
240	239	rpxrd 11305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
241	240	ad2ant2r 745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
242		xrltletr 11413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
243	227, 235, 241, 242	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
244	222, 243	mpan2d 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245	244	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
246	18	ad6antr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
247		simpllr 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
248		ffvelrn 6007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
249		xp1st 6814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
250	248, 249	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
251	247, 229, 250	syl2an 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
252		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
253	252	ad3antlr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
254		xmetcl 21126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
255	246, 251, 253, 254	syl3anc 1230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$