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 30211

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 4460	. . . . . . . . . . 11
2	1	imbi2d 316	. . . . . . . . . 10
3	2	2ralbidv 2901	. . . . . . . . 9
4	3	rexbidv 2968	. . . . . . . 8
5	4	cbvralv 3084	. . . . . . 7
6		r19.12 2983	. . . . . . . 8
7	6	ralimi 2850	. . . . . . 7
8	5, 7	sylbi 195	. . . . . 6
9		rphalfcl 11269	. . . . . . . . 9
10		breq2 4460	. . . . . . . . . . . . . . . 16
11	10	imbi2d 316	. . . . . . . . . . . . . . 15
12	11	ralbidv 2896	. . . . . . . . . . . . . 14
13	12	rexbidv 2968	. . . . . . . . . . . . 13
14	13	ralbidv 2896	. . . . . . . . . . . 12
15	14	rspcva 3208	. . . . . . . . . . 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 11269	. . . . . . . . . . . . . . . . . . . . . . 23
22	21	rpxrd 11282	. . . . . . . . . . . . . . . . . . . . . 22
23		eqid 2457	. . . . . . . . . . . . . . . . . . . . . . . 24
24	23	blopn 21128	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
25	24	3expa 1196	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
26	20, 22, 25	syl2an 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
27	26	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
28	21	rpgt0d 11284	. . . . . . . . . . . . . . . . . . . . . . 23
29	22, 28	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
30		xblcntr 21039	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
31	30	3expa 1196	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
32	20, 29, 31	syl2an 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
33	32	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
34		opelxpi 5040	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
35	21, 34	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
36	35	adantll 713	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
37	36	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
38		rpcn 11253	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
39	38	2halvesd 10805	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
40	39	breq2d 4468	. . . . . . . . . . . . . . . . . . . . . . . . . 26
41	40	imbi1d 317	. . . . . . . . . . . . . . . . . . . . . . . . 25
42	41	ralbidv 2896	. . . . . . . . . . . . . . . . . . . . . . . 24
43		oveq2 6304	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
44	43	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . 26
45		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
46	45	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
47	46	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . 26
48	44, 47	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	48	cbvralv 3084	. . . . . . . . . . . . . . . . . . . . . . . 24
50	42, 49	syl6bb 261	. . . . . . . . . . . . . . . . . . . . . . 23
51	50	biimpar 485	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
52	51	adantll 713	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
53		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
54		ovex 6324	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
55	53, 54	op1std 6809	. . . . . . . . . . . . . . . . . . . . . . . . . 26
56	53, 54	op2ndd 6810	. . . . . . . . . . . . . . . . . . . . . . . . . 26
57	55, 56	oveq12d 6314	. . . . . . . . . . . . . . . . . . . . . . . . 25
58	57	eqcomd 2465	. . . . . . . . . . . . . . . . . . . . . . . 24
59	58	biantrurd 508	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
60	55	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . 26
61	56, 56	oveq12d 6314	. . . . . . . . . . . . . . . . . . . . . . . . . 26
62	60, 61	breq12d 4469	. . . . . . . . . . . . . . . . . . . . . . . . 25
63	55	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
64	63	oveq1d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . 26
65	64	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . 25
66	62, 65	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . 24
67	66	ralbidv 2896	. . . . . . . . . . . . . . . . . . . . . . 23
68	59, 67	bitr3d 255	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
69	68	rspcev 3210	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
70	37, 52, 69	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71		eleq2 2530	. . . . . . . . . . . . . . . . . . . . . 22
72		eqeq1 2461	. . . . . . . . . . . . . . . . . . . . . . . 24
73	72	anbi1d 704	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
74	73	rexbidv 2968	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
75	71, 74	anbi12d 710	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
76	75	rspcev 3210	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
77	27, 33, 70, 76	syl12anc 1226	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	77	ex 434	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
79	78	rexlimdva 2949	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
80	79	ralimdva 2865	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
81	80	imp 429	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
82	23	mopnuni 21069	. . . . . . . . . . . . . . . . . 18
83	18, 82	syl 16	. . . . . . . . . . . . . . . . 17
84	83	raleqdv 3060	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
85	84	ad3antrrr 729	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86	81, 85	mpbid 210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
87		eqid 2457	. . . . . . . . . . . . . . 15
88		fveq2 5872	. . . . . . . . . . . . . . . . . 18
89		fveq2 5872	. . . . . . . . . . . . . . . . . 18
90	88, 89	oveq12d 6314	. . . . . . . . . . . . . . . . 17
91	90	eqeq2d 2471	. . . . . . . . . . . . . . . 16
92	88	oveq1d 6311	. . . . . . . . . . . . . . . . . . 19
93	89, 89	oveq12d 6314	. . . . . . . . . . . . . . . . . . 19
94	92, 93	breq12d 4469	. . . . . . . . . . . . . . . . . 18
95	88	fveq2d 5876	. . . . . . . . . . . . . . . . . . . 20
96	95	oveq1d 6311	. . . . . . . . . . . . . . . . . . 19
97	96	breq1d 4466	. . . . . . . . . . . . . . . . . 18
98	94, 97	imbi12d 320	. . . . . . . . . . . . . . . . 17
99	98	ralbidv 2896	. . . . . . . . . . . . . . . 16
100	91, 99	anbi12d 710	. . . . . . . . . . . . . . 15 $/\$ $/\$
101	87, 100	cmpcovf 20017	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102	17, 86, 101	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	102	ex 434	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
104		inss2 3715	. . . . . . . . . . . . . . 15
105	104	sseli 3495	. . . . . . . . . . . . . 14
106		simpll 753	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	106	anim1i 568	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
108		frn 5743	. . . . . . . . . . . . . . . . . . . . . . . 24
109		rnss 5241	. . . . . . . . . . . . . . . . . . . . . . . 24
110	108, 109	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23
111		rnxpss 5446	. . . . . . . . . . . . . . . . . . . . . . 23
112	110, 111	syl6ss 3511	. . . . . . . . . . . . . . . . . . . . . 22
113	112	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
114		simplr 755	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
115		ffun 5739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
116		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
117	116	fundmen 7608	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
118	117	ensymd 7585	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
119	115, 118	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26
120		fdm 5741	. . . . . . . . . . . . . . . . . . . . . . . . . 26
121	119, 120	breqtrd 4480	. . . . . . . . . . . . . . . . . . . . . . . . 25
122		enfii 7756	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
123	121, 122	sylan2 474	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
124		rnfi 7823	. . . . . . . . . . . . . . . . . . . . . . . 24
125		rnfi 7823	. . . . . . . . . . . . . . . . . . . . . . . 24
126	123, 124, 125	3syl 20	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
127	114, 126	sylan 471	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
128	120	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
129		eqtr 2483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
130	83, 129	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
131		heicant.x	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
132	131	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
133	130, 132	eqnetrrd 2751	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
134		unieq 4259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
135		uni0 4278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
136	134, 135	syl6eq 2514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
137	136	necon3i 2697	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
138	133, 137	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
139	138	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
140	128, 139	eqnetrd 2750	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
141		dm0rn0 5229	. . . . . . . . . . . . . . . . . . . . . . . . . 26
142	141	necon3bii 2725	. . . . . . . . . . . . . . . . . . . . . . . . 25
143	140, 142	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
144		relxp 5119	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
145		relss 5099	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
146	108, 144, 145	mpisyl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26
147		relrn0 5270	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
148	147	necon3bid 2715	. . . . . . . . . . . . . . . . . . . . . . . . . 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 11255	. . . . . . . . . . . . . . . . . . . . . . 23
154	113, 153	syl6ss 3511	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
155		gtso 9683	. . . . . . . . . . . . . . . . . . . . . . 23
156		fisupcl 7945	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
157	155, 156	mpan 670	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
158	127, 152, 154, 157	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
159	113, 158	sseldd 3500	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
160	107, 159	sylanl1 650	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
161	160	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	83	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
163	162	anim1i 568	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
164	163	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
165		simpl 457	. . . . . . . . . . . . . . . . . . . . 21 $/\$
166	129	eleq2d 2527	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
167		eluni2 4255	. . . . . . . . . . . . . . . . . . . . . . 23
168	166, 167	syl6bb 261	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
169	168	biimpa 484	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
170	164, 165, 169	syl2an 477	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
171		nfv 1708	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
172		nfra1 2838	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
173	171, 172	nfan 1929	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
174		nfv 1708	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
175	173, 174	nfan 1929	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176		nfv 1708	. . . . . . . . . . . . . . . . . . . . 21
177		rspa 2824	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
178		oveq2 6304	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
179	178	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
180		fveq2 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
181	180	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
182	181	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
183	179, 182	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
184	183	rspcva 3208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
185		oveq2 6304	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
186	185	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
187	45	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
188	187	breq1d 4466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
189	186, 188	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
190	189	rspcva 3208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
191	184, 190	anim12i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$
192	191	anandirs 831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
193		prth 571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$
194	192, 193	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$
195	194	adantrl 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
196	195	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
197	196	adantlll 717	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
198		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
199	198	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
200	199	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
201	112, 153	syl6ss 3511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
202	201	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
203		0re 9613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
204		rpge0 11257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
205	204	rgen 2817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
206		ssralv 3560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
207	112, 205, 206	mpisyl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
208		breq1 4459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
209	208	ralbidv 2896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
210	209	rspcev 3210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
211	203, 207, 210	sylancr 663	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
212	211	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
213	146	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
214		ffn 5737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
215		fnfvelrn 6029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
216	214, 215	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
217		2ndrn 6847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
218	213, 216, 217	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
219		infmrlb 10544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
220	202, 212, 218, 219	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
221	220	adantll 713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
222	221	ad2ant2r 746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
223	18	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
224		xmetcl 20959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
225	224	3expb 1197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
226	223, 225	sylan 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
227	226	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
228		simplr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
229		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
230		ne0i 3799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
231	218, 230	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
232		infmrcl 10542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
233	202, 231, 212, 232	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
234	233	rexrd 9660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
235	228, 229, 234	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
236		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
237	236	ffvelrnda 6032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
238		xp2nd 6830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
239	237, 238	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$
240	239	rpxrd 11282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$
241	240	ad2ant2r 746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
242		xrltletr 11385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
243	227, 235, 241, 242	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
244	222, 243	mpan2d 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
245	244	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
246	18	ad6antr 735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
247		simpllr 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
248		ffvelrn 6030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
249		xp1st 6829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
250	248, 249	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
251	247, 229, 250	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
252		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
253	252	ad3antlr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
254		xmetcl 20959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
255	246, 251, 253, 254	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$