poimirlem4 - Mathbox for Brendan Leahy

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

Theorem poimirlem4 33413

Description: Lemma for poimir 33442 connecting the admissible faces on the back face of the

-cube to admissible simplices in the

-cube. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem4.1
poimirlem4.2
poimirlem4.3

**Assertion**
Ref	Expression
poimirlem4	..^ ..^ $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem poimirlem4 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimir.0	. . . . . . . 8
2	1	adantr 481	. . . . . . 7 $/\$ ..^
3		poimirlem4.1	. . . . . . . 8
4	3	adantr 481	. . . . . . 7 $/\$ ..^
5		poimirlem4.2	. . . . . . . 8
6	5	adantr 481	. . . . . . 7 $/\$ ..^
7		poimirlem4.3	. . . . . . . 8
8	7	adantr 481	. . . . . . 7 $/\$ ..^
9		xp1st 7198	. . . . . . . . 9 ..^ ..^
10		elmapi 7879	. . . . . . . . 9 ..^ ..^
11	9, 10	syl 17	. . . . . . . 8 ..^ ..^
12	11	adantl 482	. . . . . . 7 $/\$ ..^ ..^
13		xp2nd 7199	. . . . . . . . 9 ..^
14		fvex 6201	. . . . . . . . . 10
15		f1oeq1 6127	. . . . . . . . . 10
16	14, 15	elab 3350	. . . . . . . . 9
17	13, 16	sylib 208	. . . . . . . 8 ..^
18	17	adantl 482	. . . . . . 7 $/\$ ..^
19	2, 4, 6, 8, 12, 18	poimirlem3 33412	. . . . . 6 $/\$ ..^ ..^ $/\$ $/\$ $/\$
20		fvex 6201	. . . . . . . . . . . . . . . 16
21		snex 4908	. . . . . . . . . . . . . . . 16
22	20, 21	unex 6956	. . . . . . . . . . . . . . 15
23		snex 4908	. . . . . . . . . . . . . . . 16
24	14, 23	unex 6956	. . . . . . . . . . . . . . 15
25	22, 24	op1std 7178	. . . . . . . . . . . . . 14
26	22, 24	op2ndd 7179	. . . . . . . . . . . . . . . . 17
27	26	imaeq1d 5465	. . . . . . . . . . . . . . . 16
28	27	xpeq1d 5138	. . . . . . . . . . . . . . 15
29	26	imaeq1d 5465	. . . . . . . . . . . . . . . 16
30	29	xpeq1d 5138	. . . . . . . . . . . . . . 15
31	28, 30	uneq12d 3768	. . . . . . . . . . . . . 14
32	25, 31	oveq12d 6668	. . . . . . . . . . . . 13
33	32	uneq1d 3766	. . . . . . . . . . . 12
34	33	csbeq1d 3540	. . . . . . . . . . 11
35	34	eqeq2d 2632	. . . . . . . . . 10
36	35	rexbidv 3052	. . . . . . . . 9
37	36	ralbidv 2986	. . . . . . . 8
38	25	fveq1d 6193	. . . . . . . . 9
39	38	eqeq1d 2624	. . . . . . . 8
40	26	fveq1d 6193	. . . . . . . . 9
41	40	eqeq1d 2624	. . . . . . . 8
42	37, 39, 41	3anbi123d 1399	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
43	42	elrab 3363	. . . . . 6 ..^ $/\$ $/\$ ..^ $/\$ $/\$ $/\$
44	19, 43	syl6ibr 242	. . . . 5 $/\$ ..^ ..^ $/\$ $/\$
45	44	ralrimiva 2966	. . . 4 ..^ ..^ $/\$ $/\$
46		fveq2 6191	. . . . . . . . . . 11
47		fveq2 6191	. . . . . . . . . . . . . 14
48	47	imaeq1d 5465	. . . . . . . . . . . . 13
49	48	xpeq1d 5138	. . . . . . . . . . . 12
50	47	imaeq1d 5465	. . . . . . . . . . . . 13
51	50	xpeq1d 5138	. . . . . . . . . . . 12
52	49, 51	uneq12d 3768	. . . . . . . . . . 11
53	46, 52	oveq12d 6668	. . . . . . . . . 10
54	53	uneq1d 3766	. . . . . . . . 9
55	54	csbeq1d 3540	. . . . . . . 8
56	55	eqeq2d 2632	. . . . . . 7
57	56	rexbidv 3052	. . . . . 6
58	57	ralbidv 2986	. . . . 5
59	58	ralrab 3368	. . . 4 ..^ ..^ $/\$ $/\$ ..^ ..^ $/\$ $/\$
60	45, 59	sylibr 224	. . 3 ..^ ..^ $/\$ $/\$
61		xp1st 7198	. . . . . . . . . . . . . . 15 ..^ ..^
62		elmapi 7879	. . . . . . . . . . . . . . 15 ..^ ..^
63	61, 62	syl 17	. . . . . . . . . . . . . 14 ..^ ..^
64		fzssp1 12384	. . . . . . . . . . . . . 14
65		fssres 6070	. . . . . . . . . . . . . 14 ..^ $/\$ ..^
66	63, 64, 65	sylancl 694	. . . . . . . . . . . . 13 ..^ ..^
67		ovex 6678	. . . . . . . . . . . . . 14 ..^
68		ovex 6678	. . . . . . . . . . . . . 14
69	67, 68	elmap 7886	. . . . . . . . . . . . 13 ..^ ..^
70	66, 69	sylibr 224	. . . . . . . . . . . 12 ..^ ..^
71	70	ad2antlr 763	. . . . . . . . . . 11 $/\$ ..^ $/\$ ..^
72		xp2nd 7199	. . . . . . . . . . . . . . . . 17 ..^
73		fvex 6201	. . . . . . . . . . . . . . . . . 18
74		f1oeq1 6127	. . . . . . . . . . . . . . . . . 18
75	73, 74	elab 3350	. . . . . . . . . . . . . . . . 17
76	72, 75	sylib 208	. . . . . . . . . . . . . . . 16 ..^
77		f1of1 6136	. . . . . . . . . . . . . . . 16
78	76, 77	syl 17	. . . . . . . . . . . . . . 15 ..^
79		f1ores 6151	. . . . . . . . . . . . . . 15 $/\$
80	78, 64, 79	sylancl 694	. . . . . . . . . . . . . 14 ..^
81	80	ad2antlr 763	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
82		dff1o3 6143	. . . . . . . . . . . . . . . . . . 19 $/\$
83	82	simprbi 480	. . . . . . . . . . . . . . . . . 18
84		imadif 5973	. . . . . . . . . . . . . . . . . 18 $\$ $\$
85	76, 83, 84	3syl 18	. . . . . . . . . . . . . . . . 17 ..^ $\$ $\$
86	85	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $\$ $\$
87		f1ofo 6144	. . . . . . . . . . . . . . . . . . 19
88		foima 6120	. . . . . . . . . . . . . . . . . . 19
89	76, 87, 88	3syl 18	. . . . . . . . . . . . . . . . . 18 ..^
90	89	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
91		f1ofn 6138	. . . . . . . . . . . . . . . . . . . 20
92	76, 91	syl 17	. . . . . . . . . . . . . . . . . . 19 ..^
93		nn0p1nn 11332	. . . . . . . . . . . . . . . . . . . . 21
94	5, 93	syl 17	. . . . . . . . . . . . . . . . . . . 20
95		elfz1end 12371	. . . . . . . . . . . . . . . . . . . 20
96	94, 95	sylib 208	. . . . . . . . . . . . . . . . . . 19
97		fnsnfv 6258	. . . . . . . . . . . . . . . . . . 19 $/\$
98	92, 96, 97	syl2anr 495	. . . . . . . . . . . . . . . . . 18 $/\$ ..^
99		sneq 4187	. . . . . . . . . . . . . . . . . 18
100	98, 99	sylan9req 2677	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$
101	90, 100	difeq12d 3729	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $\$ $\$
102	86, 101	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $\$ $\$
103		1z 11407	. . . . . . . . . . . . . . . . . . . . 21
104		nn0uz 11722	. . . . . . . . . . . . . . . . . . . . . . 23
105		1m1e0 11089	. . . . . . . . . . . . . . . . . . . . . . . 24
106	105	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . . . 23
107	104, 106	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . . . 22
108	5, 107	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . 21
109		fzsuc2 12398	. . . . . . . . . . . . . . . . . . . . 21 $/\$
110	103, 108, 109	sylancr 695	. . . . . . . . . . . . . . . . . . . 20
111	110	difeq1d 3727	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
112		difun2 4048	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
113	111, 112	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 $\$ $\$
114	5	nn0red 11352	. . . . . . . . . . . . . . . . . . . . 21
115		ltp1 10861	. . . . . . . . . . . . . . . . . . . . . 22
116		peano2re 10209	. . . . . . . . . . . . . . . . . . . . . . 23
117		ltnle 10117	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
118	116, 117	mpdan 702	. . . . . . . . . . . . . . . . . . . . . 22
119	115, 118	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21
120	114, 119	syl 17	. . . . . . . . . . . . . . . . . . . 20
121		elfzle2 12345	. . . . . . . . . . . . . . . . . . . 20
122	120, 121	nsyl 135	. . . . . . . . . . . . . . . . . . 19
123		difsn 4328	. . . . . . . . . . . . . . . . . . 19 $\$
124	122, 123	syl 17	. . . . . . . . . . . . . . . . . 18 $\$
125	113, 124	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $\$
126	125	imaeq2d 5466	. . . . . . . . . . . . . . . 16 $\$
127	126	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $\$
128	125	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $\$
129	102, 127, 128	3eqtr3d 2664	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$
130		f1oeq3 6129	. . . . . . . . . . . . . 14
131	129, 130	syl 17	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
132	81, 131	mpbid 222	. . . . . . . . . . . 12 $/\$ ..^ $/\$
133	73	resex 5443	. . . . . . . . . . . . 13
134		f1oeq1 6127	. . . . . . . . . . . . 13
135	133, 134	elab 3350	. . . . . . . . . . . 12
136	132, 135	sylibr 224	. . . . . . . . . . 11 $/\$ ..^ $/\$
137		opelxpi 5148	. . . . . . . . . . 11 ..^ $/\$ ..^
138	71, 136, 137	syl2anc 693	. . . . . . . . . 10 $/\$ ..^ $/\$ ..^
139	138	3ad2antr3 1228	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$ $/\$ ..^
140		3anass 1042	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
141		ancom 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
142	140, 141	bitri 264	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
143	94	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . . 25
144		uzid 11702	. . . . . . . . . . . . . . . . . . . . . . . . 25
145		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . . 25
146	143, 144, 145	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24
147	5	nn0zd 11480	. . . . . . . . . . . . . . . . . . . . . . . . . 26
148	1	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . . . 26
149		zltp1le 11427	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
150		peano2z 11418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
151		eluz 11701	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
152	150, 151	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
153	149, 152	bitr4d 271	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
154	147, 148, 153	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25
155	7, 154	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . 24
156		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
157	146, 155, 156	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23
158		fzsn 12383	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	143, 158	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
160	159	uneq1d 3766	. . . . . . . . . . . . . . . . . . . . . . 23
161	157, 160	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . 22
162	161	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . 21
163	162	uneq2d 3767	. . . . . . . . . . . . . . . . . . . 20
164		xpundir 5172	. . . . . . . . . . . . . . . . . . . . . . 23
165		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . 25
166		c0ex 10034	. . . . . . . . . . . . . . . . . . . . . . . . 25
167	165, 166	xpsn 6407	. . . . . . . . . . . . . . . . . . . . . . . 24
168	167	uneq1i 3763	. . . . . . . . . . . . . . . . . . . . . . 23
169	164, 168	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . 22
170	169	uneq2i 3764	. . . . . . . . . . . . . . . . . . . . 21
171		unass 3770	. . . . . . . . . . . . . . . . . . . . 21
172	170, 171	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . 20
173	163, 172	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19
174	173	ad3antrrr 766	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
175	165	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$ $/\$
176	166	a1i 11	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$ $/\$
177	110	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . 21
178	177	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$ $/\$
179		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22
180		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22
181	179, 180	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . 21
182		simplrl 800	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$ $/\$
183		imain 5974	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
184	76, 83, 183	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
185	184	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$
186		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
187	186	nn0red 11352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
188	187	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
189		fzdisj 12368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
190	188, 189	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
191	190	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
192		ima0 5481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
193	191, 192	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
194	185, 193	sylan9req 2677	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$ $/\$
195		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ $/\$
196	92	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^ $/\$
197		nn0p1nn 11332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
198		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
199	197, 198	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
200		fzss1 12380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
201	186, 199, 200	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
202		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
203		eluzp1p1 11713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
204		eluzfz2 12349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
205	202, 203, 204	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
206	201, 205	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
207		fnfvima 6496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
208	207	3expb 1266	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
209	196, 206, 208	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ $/\$
210	195, 209	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$ $/\$
211		1ex 10035	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
212		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
213	211, 212	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
214		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
215	166, 214	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
216		fvun2 6270	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
217	213, 215, 216	mp3an12 1414	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
218	194, 210, 217	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
219	166	fvconst2 6469	. . . . . . . . . . . . . . . . . . . . . . . . . 26
220	210, 219	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$
221	218, 220	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$
222	221	adantlrl 756	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$ $/\$
223	182, 222	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$ $/\$
224		00id 10211	. . . . . . . . . . . . . . . . . . . . . 22
225	223, 224	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$ $/\$
226	181, 225	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$ $/\$ $/\$
227	175, 176, 178, 226	fmptapd 6437	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$ $/\$
228	227	uneq1d 3766	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ $/\$
229	174, 228	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
230		elmapfn 7880	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
231	61, 230	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ..^
232		fnssres 6004	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
233	231, 64, 232	sylancl 694	. . . . . . . . . . . . . . . . . . . . 21 ..^
234	233	ad3antlr 767	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
235		simplr 792	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ ..^
236		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . . . . . . 26
237	166, 236	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . 25
238	213, 237	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
239		imain 5974	. . . . . . . . . . . . . . . . . . . . . . . . . 26
240	76, 83, 239	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
241		fzdisj 12368	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
242	188, 241	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
243	242	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . 26
244	243, 192	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . 25
245	240, 244	sylan9req 2677	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$
246		fnun 5997	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
247	238, 245, 246	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . 23 ..^ $/\$
248	235, 247	sylan 488	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
249	101	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$ $\$ $\$
250	85	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$ $/\$ $\$ $\$
251	186, 197	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
252	251, 198	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
253		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
254	252, 202, 253	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
255	128, 254	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^ $/\$ $/\$ $\$
256	255	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$ $/\$ $\$
257	250, 256	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$ $\$
258	125	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$ $/\$ $\$
259	249, 257, 258	3eqtr3rd 2665	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$
260		imaundi 5545	. . . . . . . . . . . . . . . . . . . . . . . 24
261	259, 260	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
262	261	fneq2d 5982	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
263	248, 262	mpbird 247	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
264		fzss2 12381	. . . . . . . . . . . . . . . . . . . . . . . . . 26
265		resima2 5432	. . . . . . . . . . . . . . . . . . . . . . . . . 26
266	202, 264, 265	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25
267	266	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . 24
268	186, 199	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
269		fzss1 12380	. . . . . . . . . . . . . . . . . . . . . . . . . 26
270		resima2 5432	. . . . . . . . . . . . . . . . . . . . . . . . . 26
271	268, 269, 270	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25
272	271	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . 24
273	267, 272	uneq12d 3768	. . . . . . . . . . . . . . . . . . . . . . 23
274	273	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
275	274	fneq1d 5981	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$
276	263, 275	mpbird 247	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
277		fzfid 12772	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$
278		inidm 3822	. . . . . . . . . . . . . . . . . . . 20
279		fvres 6207	. . . . . . . . . . . . . . . . . . . . 21
280	279	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$ $/\$
281		disjsn 4246	. . . . . . . . . . . . . . . . . . . . . . . . 25
282	122, 281	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . 24
283	282	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
284	263, 283	jca 554	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$ $/\$
285		fnconstg 6093	. . . . . . . . . . . . . . . . . . . . . . . . 25
286	166, 285	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24
287		fvun1 6269	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
288	286, 287	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
289	288	anassrs 680	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
290	284, 289	sylan 488	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$ $/\$
291	251	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
292	186	nn0cnd 11353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
293		pncan1 10454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
294	292, 293	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
295	294	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
296	202, 295	eleqtrrd 2704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
297		fzsuc2 12398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
298	291, 296, 297	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
299	298	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
300		imaundi 5545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
301	299, 300	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
302	301	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
303		xpundir 5172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
304	302, 303	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
305	304	uneq2d 3767	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
306		unass 3770	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
307	305, 306	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
308	307	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$
309	98	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ ..^
310	309	uneq2d 3767	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^
311	310	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^ $/\$
312	308, 311	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ ..^ $/\$
313	99	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . . . . . . 26
314	313	uneq2d 3767	. . . . . . . . . . . . . . . . . . . . . . . . 25
315	312, 314	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ ..^ $/\$ $/\$
316	315	an32s 846	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ ..^ $/\$ $/\$
317	316	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ ..^ $/\$ $/\$
318	317	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$ $/\$
319	273	fveq1d 6193	. . . . . . . . . . . . . . . . . . . . . 22
320	319	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . 21 $/\$ ..^ $/\$ $/\$ $/\$
321	290, 318, 320	3eqtr4rd 2667	. . . . . . . . . . . . . . . . . . . 20 $/\$ ..^ $/\$ $/\$ $/\$
322	234, 276, 277, 277, 278, 280, 321	offval 6904	. . . . . . . . . . . . . . . . . . 19 $/\$ ..^ $/\$ $/\$
323	322	uneq1d 3766	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$
324	323	adantlrl 756	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
325		simplr 792	. . . . . . . . . . . . . . . . . 18 $/\$ ..^ $/\$ $/\$ ..^
326	231	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
327	213, 215	pm3.2i 471	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
328	184, 193	sylan9req 2677	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
329		fnun 5997	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
330	327, 328, 329	sylancr 695	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
331		peano2uz 11741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
332	202, 331	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26
333		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
334	268, 332, 333	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25
335	334	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . . . 24
336		imaundi 5545	. . . . . . . . . . . . . . . . . . . . . . . 24
337	335, 336	syl6req 2673	. . . . . . . . . . . . . . . . . . . . . . 23
338	337, 89	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . 22 ..^ $/\$
339	338	fneq2d 5982	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$
340	330, 339	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
341		fzfid 12772	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$
342		inidm 3822	. . . . . . . . . . . . . . . . . . . 20
343		eqidd 2623	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$ $/\$
344		eqidd 2623	. . . . . . . . . . . . . . . . . . . 20 ..^ $/\$ $/\$
345	326, 340, 341, 341, 342, 343, 344	offval 6904	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
346	345	uneq1d 3766	. . . . . . . . . . . . . . . . . 18 ..^ $/\$
347	325, 346	sylan 488	. . . . . . . . . . . . . . . . 17 $/\$ ..^ $/\$ $/\$ $/\$
348	229, 324, 347	3eqtr4rd 2667	. . . . . . . . . . . . . . . 16 $/\$ ..^ $/\$ $/\$ $/\$
349	348	csbeq1d 3540	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$ $/\$ $/\$
350	349	eqeq2d 2632	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ $/\$
351	350	rexbidva 3049	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ $/\$
352	351	ralbidv 2986	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
353	352	biimpd 219	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
354	353	impr 649	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$ $/\$
355	142, 354	sylan2b 492	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$ $/\$
356		1st2nd2 7205	. . . . . . . . . . . 12 ..^
357	356	ad2antlr 763	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
358		fnsnsplit 6450	. . . . . . . . . . . . . . . 16 $/\$ $\$
359	231, 96, 358	syl2anr 495	. . . . . . . . . . . . . . 15 $/\$ ..^ $\$
360	359	adantr 481	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $\$
361	125	reseq2d 5396	. . . . . . . . . . . . . . . 16 $\$
362	361	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^ $\$
363		opeq2 4403	. . . . . . . . . . . . . . . 16
364	363	sneqd 4189	. . . . . . . . . . . . . . 15
365		uneq12 3762	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
366	362, 364, 365	syl2an 494	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $\$
367	360, 366	eqtrd 2656	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
368	367	adantrr 753	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
369		fnsnsplit 6450	. . . . . . . . . . . . . . . 16 $/\$ $\$
370	92, 96, 369	syl2anr 495	. . . . . . . . . . . . . . 15 $/\$ ..^ $\$
371	370	adantr 481	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $\$
372	125	reseq2d 5396	. . . . . . . . . . . . . . . 16 $\$
373	372	adantr 481	. . . . . . . . . . . . . . 15 $/\$ ..^ $\$
374		opeq2 4403	. . . . . . . . . . . . . . . 16
375	374	sneqd 4189	. . . . . . . . . . . . . . 15
376		uneq12 3762	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$
377	373, 375, 376	syl2an 494	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $\$
378	371, 377	eqtrd 2656	. . . . . . . . . . . . 13 $/\$ ..^ $/\$
379	378	adantrl 752	. . . . . . . . . . . 12 $/\$ ..^ $/\$ $/\$
380	368, 379	opeq12d 4410	. . . . . . . . . . 11 $/\$ ..^ $/\$ $/\$
381	357, 380	eqtrd 2656	. . . . . . . . . 10 $/\$ ..^ $/\$ $/\$
382	381	3adantr1 1220	. . . . . . . . 9 $/\$ ..^ $/\$ $/\$ $/\$
383		fvex 6201	. . . . . . . . . . . . . . . . . . 19
384	383	resex 5443	. . . . . . . . . . . . . . . . . 18
385	384, 133	op1std 7178	. . . . . . . . . . . . . . . . 17
386	384, 133	op2ndd 7179	. . . . . . . . . . . . . . . . . . . 20
387	386	imaeq1d 5465	. . . . . . . . . . . . . . . . . . 19
388	387	xpeq1d 5138	. . . . . . . . . . . . . . . . . 18
389	386	imaeq1d 5465	. . . . . . . . . . . . . . . . . . 19
390	389	xpeq1d 5138	. . . . . . . . . . . . . . . . . 18
391	388, 390	uneq12d 3768	. . . . . . . . . . . . . . . . 17
392	385, 391	oveq12d 6668	. . . . . . . . . . . . . . . 16
393	392	uneq1d 3766	. . . . . . . . . . . . . . 15
394	393	csbeq1d 3540	. . . . . . . . . . . . . 14
395	394	eqeq2d 2632	. . . . . . . . . . . . 13
396	395	rexbidv 3052	. . . . . . . . . . . 12
397	396	ralbidv 2986	. . . . . . . . . . 11
398	385	uneq1d 3766	. . . . . . . . . . . . 13
399	386	uneq1d 3766	. . . . . . . . . . . . 13
400	398, 399	opeq12d 4410	. . . . . . . . . . . 12
401	400	eqeq2d 2632	. . . . . . . . . . 11
402	397, 401	anbi12d 747	. . . . . . . . . 10 $/\$ $/\$
403	402	rspcev 3309	. . . . . . . . 9 ..^ $/\$ $/\$ ..^ $/\$
404	139, 355, 382, 403	syl12anc 1324	. . . . . . . 8 $/\$ ..^ $/\$ $/\$ $/\$ ..^ $/\$
405	404	ex 450	. . . . . . 7 $/\$ ..^ $/\$ $/\$ ..^ $/\$
406		elrabi 3359	. . . . . . . . . . 11 ..^ ..^
407		elrabi 3359	. . . . . . . . . . 11 ..^ ..^
408	406, 407	anim12i 590	. . . . . . . . . 10 ..^ $/\$ ..^ ..^ $/\$ ..^
409		eqtr2 2642	. . . . . . . . . . . 12 $/\$
410	22, 24	opth 4945	. . . . . . . . . . . . 13 $/\$
411		difeq1 3721	. . . . . . . . . . . . . . 15 $\$ $\$
412		difun2 4048	. . . . . . . . . . . . . . 15 $\$ $\$
413		difun2 4048	. . . . . . . . . . . . . . 15 $\$ $\$
414	411, 412, 413	3eqtr3g 2679	. . . . . . . . . . . . . 14 $\$ $\$
415		difeq1 3721	. . . . . . . . . . . . . . 15 $\$ $\$
416		difun2 4048	. . . . . . . . . . . . . . 15 $\$ $\$
417		difun2 4048	. . . . . . . . . . . . . . 15 $\$ $\$
418	415, 416, 417	3eqtr3g 2679	. . . . . . . . . . . . . 14 $\$ $\$
419	414, 418	anim12i 590	. . . . . . . . . . . . 13 $/\$ $\$ $\$ $/\$ $\$ $\$
420	410, 419	sylbi 207	. . . . . . . . . . . 12 $\$ $\$ $/\$ $\$ $\$
421	409, 420	syl 17	. . . . . . . . . . 11 $/\$ $\$ $\$ $/\$ $\$ $\$
422		elmapfn 7880	. . . . . . . . . . . . . . . . . . 19 ..^
423		fnop 5994	. . . . . . . . . . . . . . . . . . . 20 $/\$
424	423	ex 450	. . . . . . . . . . . . . . . . . . 19
425	9, 422, 424	3syl 18	. . . . . . . . . . . . . . . . . 18 ..^
426	425, 122	nsyli 155	. . . . . . . . . . . . . . . . 17 ..^
427	426	impcom 446	. . . . . . . . . . . . . . . 16 $/\$ ..^
428		difsn 4328	. . . . . . . . . . . . . . . 16 $\$
429	427, 428	syl 17	. . . . . . . . . . . . . . 15 $/\$ ..^ $\$
430		xp1st 7198	. . . . . . . . . . . . . . . . . . 19 ..^ ..^
431		elmapfn 7880	. . . . . . . . . . . . . . . . . . 19 ..^
432		fnop 5994	. . . . . . . . . . . . . . . . . . . 20 $/\$
433	432	ex 450	. . . . . . . . . . . . . . . . . . 19
434	430, 431, 433	3syl 18	. . . . . . . . . . . . . . . . . 18 ..^
435	434, 122	nsyli 155	. . . . . . . . . . . . . . . . 17 ..^
436	435	impcom 446	. . . . . . . . . . . . . . . 16 $/\$ ..^
437		difsn 4328	. . . . . . . . . . . . . . . 16 $\$
438	436, 437	syl 17	. . . . . . . . . . . . . . 15 $/\$ ..^ $\$
439	429, 438	eqeqan12d 2638	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ ..^ $\$ $\$
440	439	anandis 873	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^ $\$ $\$
441		f1ofn 6138	. . . . . . . . . . . . . . . . . . 19
442		fnop 5994	. . . . . . . . . . . . . . . . . . . 20 $/\$
443	442	ex 450	. . . . . . . . . . . . . . . . . . 19
444	17, 441, 443	3syl 18	. . . . . . . . . . . . . . . . . 18 ..^
445	444, 122	nsyli 155	. . . . . . . . . . . . . . . . 17 ..^
446	445	impcom 446	. . . . . . . . . . . . . . . 16 $/\$ ..^
447		difsn 4328	. . . . . . . . . . . . . . . 16 $\$
448	446, 447	syl 17	. . . . . . . . . . . . . . 15 $/\$ ..^ $\$
449		xp2nd 7199	. . . . . . . . . . . . . . . . . . . 20 ..^
450		fvex 6201	. . . . . . . . . . . . . . . . . . . . 21
451		f1oeq1 6127	. . . . . . . . . . . . . . . . . . . . 21
452	450, 451	elab 3350	. . . . . . . . . . . . . . . . . . . 20
453	449, 452	sylib 208	. . . . . . . . . . . . . . . . . . 19 ..^
454		f1ofn 6138	. . . . . . . . . . . . . . . . . . 19
455		fnop 5994	. . . . . . . . . . . . . . . . . . . 20 $/\$
456	455	ex 450	. . . . . . . . . . . . . . . . . . 19
457	453, 454, 456	3syl 18	. . . . . . . . . . . . . . . . . 18 ..^
458	457, 122	nsyli 155	. . . . . . . . . . . . . . . . 17 ..^
459	458	impcom 446	. . . . . . . . . . . . . . . 16 $/\$ ..^
460		difsn 4328	. . . . . . . . . . . . . . . 16 $\$
461	459, 460	syl 17	. . . . . . . . . . . . . . 15 $/\$ ..^ $\$
462	448, 461	eqeqan12d 2638	. . . . . . . . . . . . . 14 $/\$ ..^ $/\$ $/\$ ..^ $\$ $\$
463	462	anandis 873	. . . . . . . . . . . . 13 $/\$ ..^ $/\$ ..^ $\$ $\$
464	440, 463	anbi12d 747	. . . . . . . . . . . 12 $/\$ ..^ $/\$ ..^ $\$ $\$ $/\$ $\$ $\$ $/\$
465		xpopth 7207	. . . . . . . . . . . . 13 ..^ $/\$ ..^ $/\$
466	465	adantl 482	. . . . . . . . . . . 12 $/\$ ..^ $/\$ ..^ $/\$
467	464, 466	bitrd 268	. . . . . . . . . . 11 $/\$ ..^ $/\$ ..^ $\$ $\$ $/\$ $\$ $\$
468	421, 467	syl5ib 234	. . . . . . . . . 10 $/\$ ..^ $/\$ ..^ $/\$
469	408, 468	sylan2 491	. . . . . . . . 9 $/\$ ..^ $/\$ ..^ $/\$
470	469	ralrimivva 2971	. . . . . . . 8 ..^ ..^ $/\$
471	470	adantr 481	. . . . . . 7 $/\$ ..^ ..^ ..^ $/\$
472	405, 471	jctird 567	. . . . . 6 $/\$ ..^ $/\$ $/\$ ..^ $/\$ $/\$ ..^ ..^ $/\$
473		fveq2 6191	. . . . . . . . . . 11
474	473	uneq1d 3766	. . . . . . . . . 10
475		fveq2 6191	. . . . . . . . . . 11
476	475	uneq1d 3766	. . . . . . . . . 10
477	474, 476	opeq12d 4410	. . . . . . . . 9
478	477	eqeq2d 2632	. . . . . . . 8
479	478	reu4 3400	. . . . . . 7 ..^ ..^ $/\$ ..^ ..^ $/\$
480	58	rexrab 3370	. . . . . . . 8 ..^ ..^ $/\$
481	480	anbi1i 731	. . . . . . 7 ..^ $/\$ ..^ ..^ $/\$ ..^ $/\$ $/\$ ..^ ..^ $/\$
482	479, 481	bitri 264	. . . . . 6 ..^ ..^ $/\$ $/\$ ..^ ..^ $/\$
483	472, 482	syl6ibr 242	. . . . 5 $/\$ ..^ $/\$ $/\$ ..^
484	483	ralrimiva 2966	. . . 4 ..^ $/\$ $/\$ ..^
485		fveq2 6191	. . . . . . . . . . . 12
486		fveq2 6191	. . . . . . . . . . . . . . 15
487	486	imaeq1d 5465	. . . . . . . . . . . . . 14
488	487	xpeq1d 5138	. . . . . . . . . . . . 13
489	486	imaeq1d 5465	. . . . . . . . . . . . . 14
490	489	xpeq1d 5138	. . . . . . . . . . . . 13
491	488, 490	uneq12d 3768	. . . . . . . . . . . 12
492	485, 491	oveq12d 6668	. . . . . . . . . . 11
493	492	uneq1d 3766	. . . . . . . . . 10
494	493	csbeq1d 3540	. . . . . . . . 9
495	494	eqeq2d 2632	. . . . . . . 8
496	495	rexbidv 3052	. . . . . . 7
497	496	ralbidv 2986	. . . . . 6
498	485	fveq1d 6193	. . . . . . 7
499	498	eqeq1d 2624	. . . . . 6
500	486	fveq1d 6193	. . . . . . 7
501	500	eqeq1d 2624	. . . . . 6
502	497, 499, 501	3anbi123d 1399	. . . . 5 $/\$ $/\$ $/\$ $/\$
503	502	ralrab 3368	. . . 4 ..^ $/\$ $/\$ ..^ ..^ $/\$ $/\$ ..^
504	484, 503	sylibr 224	. . 3 ..^ $/\$ $/\$ ..^
505		eqid 2622	. . . 4 ..^ ..^
506	505	f1ompt 6382	. . 3 ..^ ..^ ..^ $/\$ $/\$ ..^ ..^ $/\$ $/\$ $/\$ ..^ $/\$ $/\$ ..^
507	60, 504, 506	sylanbrc 698	. 2 ..^ ..^ ..^ $/\$ $/\$
508		ovex 6678	. . . . 5 ..^
509		ovex 6678	. . . . . 6
510		f1of 6137	. . . . . . . 8
511	510	ss2abi 3674	. . . . . . 7
512	68, 68	mapval 7869	. . . . . . 7
513	511, 512	sseqtr4i 3638	. . . . . 6
514	509, 513	ssexi 4803	. . . . 5
515	508, 514	xpex 6962	. . . 4 ..^
516	515	rabex 4813	. . 3 ..^
517	516	f1oen 7976	. 2 ..^ ..^ ..^ $/\$ $/\$ ..^ ..^ $/\$ $/\$
518	507, 517	syl 17	1 ..^ ..^ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wcel 1990

cab 2608

wral 2912

wrex 2913

wreu 2914

crab 2916

cvv 3200

csb 3533 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

csn 4177

cop 4183 class class class wbr 4653

cmpt 4729

cxp 5112

ccnv 5113

cres 5116

cima 5117

wfun 5882

wfn 5883

wf 5884

wf1 5885

wfo 5886

wf1o 5887

cfv 5888 (class class class)co 6650

cof 6895

c1st 7166

c2nd 7167

cmap 7857

cen 7952

cfn 7955

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

clt 10074

cle 10075

cmin 10266

cn 11020

cn0 11292

cz 11377

cuz 11687

cfz 12326 ..^cfzo 12465

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-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

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 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-iun 4522 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-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-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-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466

This theorem is referenced by: poimirlem28 33437

W3C validator