poimirlem15 - Mathbox for Brendan Leahy

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

Theorem poimirlem15 33424

Description: Lemma for poimir 33442, that the face in poimirlem22 33431 is a face. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem22.s	..^
poimirlem22.1
poimirlem22.2
poimirlem15.3

**Assertion**
Ref	Expression
poimirlem15	$\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem poimirlem15**
Step	Hyp	Ref	Expression
1		poimirlem22.2	. . . . . 6
2		elrabi 3359	. . . . . . 7 ..^ ..^
3		poimirlem22.s	. . . . . . 7 ..^
4	2, 3	eleq2s 2719	. . . . . 6 ..^
5	1, 4	syl 17	. . . . 5 ..^
6		xp1st 7198	. . . . 5 ..^ ..^
7		xp1st 7198	. . . . 5 ..^ ..^
8	5, 6, 7	3syl 18	. . . 4 ..^
9		xp2nd 7199	. . . . . . . 8 ..^
10	5, 6, 9	3syl 18	. . . . . . 7
11		fvex 6201	. . . . . . . 8
12		f1oeq1 6127	. . . . . . . 8
13	11, 12	elab 3350	. . . . . . 7
14	10, 13	sylib 208	. . . . . 6
15		poimirlem15.3	. . . . . . . . . . . . 13
16		elfznn 12370	. . . . . . . . . . . . 13
17	15, 16	syl 17	. . . . . . . . . . . 12
18	17	nnred 11035	. . . . . . . . . . 11
19	18	ltp1d 10954	. . . . . . . . . . 11
20	18, 19	ltned 10173	. . . . . . . . . 10
21	20	necomd 2849	. . . . . . . . . 10
22		fvex 6201	. . . . . . . . . . 11
23		ovex 6678	. . . . . . . . . . 11
24		f1oprg 6181	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
25	22, 23, 23, 22, 24	mp4an 709	. . . . . . . . . 10 $/\$
26	20, 21, 25	syl2anc 693	. . . . . . . . 9
27		prcom 4267	. . . . . . . . . 10
28		f1oeq3 6129	. . . . . . . . . 10
29	27, 28	ax-mp 5	. . . . . . . . 9
30	26, 29	sylib 208	. . . . . . . 8
31		f1oi 6174	. . . . . . . 8 $\$ $\$ $\$
32		disjdif 4040	. . . . . . . . 9 $\$
33		f1oun 6156	. . . . . . . . 9 $/\$ $\$ $\$ $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
34	32, 32, 33	mpanr12 721	. . . . . . . 8 $/\$ $\$ $\$ $\$ $\$ $\$ $\$
35	30, 31, 34	sylancl 694	. . . . . . 7 $\$ $\$ $\$
36		poimir.0	. . . . . . . . . . . . . . 15
37	36	nncnd 11036	. . . . . . . . . . . . . 14
38		npcan1 10455	. . . . . . . . . . . . . 14
39	37, 38	syl 17	. . . . . . . . . . . . 13
40	36	nnzd 11481	. . . . . . . . . . . . . . 15
41		peano2zm 11420	. . . . . . . . . . . . . . 15
42	40, 41	syl 17	. . . . . . . . . . . . . 14
43		uzid 11702	. . . . . . . . . . . . . 14
44		peano2uz 11741	. . . . . . . . . . . . . 14
45	42, 43, 44	3syl 18	. . . . . . . . . . . . 13
46	39, 45	eqeltrrd 2702	. . . . . . . . . . . 12
47		fzss2 12381	. . . . . . . . . . . 12
48	46, 47	syl 17	. . . . . . . . . . 11
49	48, 15	sseldd 3604	. . . . . . . . . 10
50	17	peano2nnd 11037	. . . . . . . . . . 11
51	42	zred 11482	. . . . . . . . . . . . 13
52	36	nnred 11035	. . . . . . . . . . . . 13
53		elfzle2 12345	. . . . . . . . . . . . . 14
54	15, 53	syl 17	. . . . . . . . . . . . 13
55	52	ltm1d 10956	. . . . . . . . . . . . 13
56	18, 51, 52, 54, 55	lelttrd 10195	. . . . . . . . . . . 12
57	17	nnzd 11481	. . . . . . . . . . . . 13
58		zltp1le 11427	. . . . . . . . . . . . 13 $/\$
59	57, 40, 58	syl2anc 693	. . . . . . . . . . . 12
60	56, 59	mpbid 222	. . . . . . . . . . 11
61		fznn 12408	. . . . . . . . . . . 12 $/\$
62	40, 61	syl 17	. . . . . . . . . . 11 $/\$
63	50, 60, 62	mpbir2and 957	. . . . . . . . . 10
64		prssi 4353	. . . . . . . . . 10 $/\$
65	49, 63, 64	syl2anc 693	. . . . . . . . 9
66		undif 4049	. . . . . . . . 9 $\$
67	65, 66	sylib 208	. . . . . . . 8 $\$
68		f1oeq23 6130	. . . . . . . 8 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
69	67, 67, 68	syl2anc 693	. . . . . . 7 $\$ $\$ $\$ $\$
70	35, 69	mpbid 222	. . . . . 6 $\$
71		f1oco 6159	. . . . . 6 $/\$ $\$ $\$
72	14, 70, 71	syl2anc 693	. . . . 5 $\$
73		prex 4909	. . . . . . . 8
74		ovex 6678	. . . . . . . . 9
75		difexg 4808	. . . . . . . . 9 $\$
76		resiexg 7102	. . . . . . . . 9 $\$ $\$
77	74, 75, 76	mp2b 10	. . . . . . . 8 $\$
78	73, 77	unex 6956	. . . . . . 7 $\$
79	11, 78	coex 7118	. . . . . 6 $\$
80		f1oeq1 6127	. . . . . 6 $\$ $\$
81	79, 80	elab 3350	. . . . 5 $\$ $\$
82	72, 81	sylibr 224	. . . 4 $\$
83		opelxpi 5148	. . . 4 ..^ $/\$ $\$ $\$ ..^
84	8, 82, 83	syl2anc 693	. . 3 $\$ ..^
85		1eluzge0 11732	. . . . . 6
86		fzss1 12380	. . . . . 6
87	85, 86	ax-mp 5	. . . . 5
88	48, 87	syl6ss 3615	. . . 4
89	88, 15	sseldd 3604	. . 3
90		opelxpi 5148	. . 3 $\$ ..^ $/\$ $\$ ..^
91	84, 89, 90	syl2anc 693	. 2 $\$ ..^
92		fveq2 6191	. . . . . . . . . . . 12
93	92	breq2d 4665	. . . . . . . . . . 11
94	93	ifbid 4108	. . . . . . . . . 10
95	94	csbeq1d 3540	. . . . . . . . 9
96		fveq2 6191	. . . . . . . . . . . 12
97	96	fveq2d 6195	. . . . . . . . . . 11
98	96	fveq2d 6195	. . . . . . . . . . . . . 14
99	98	imaeq1d 5465	. . . . . . . . . . . . 13
100	99	xpeq1d 5138	. . . . . . . . . . . 12
101	98	imaeq1d 5465	. . . . . . . . . . . . 13
102	101	xpeq1d 5138	. . . . . . . . . . . 12
103	100, 102	uneq12d 3768	. . . . . . . . . . 11
104	97, 103	oveq12d 6668	. . . . . . . . . 10
105	104	csbeq2dv 3992	. . . . . . . . 9
106	95, 105	eqtrd 2656	. . . . . . . 8
107	106	mpteq2dv 4745	. . . . . . 7
108	107	eqeq2d 2632	. . . . . 6
109	108, 3	elrab2 3366	. . . . 5 ..^ $/\$
110	109	simprbi 480	. . . 4
111	1, 110	syl 17	. . 3
112		imaco 5640	. . . . . . . . . 10 $\$ $\$
113		f1ofn 6138	. . . . . . . . . . . . . . . 16
114	26, 113	syl 17	. . . . . . . . . . . . . . 15
115	114	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$
116		incom 3805	. . . . . . . . . . . . . . 15
117		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . 22
118	117	nn0red 11352	. . . . . . . . . . . . . . . . . . . . 21
119		ltnle 10117	. . . . . . . . . . . . . . . . . . . . 21 $/\$
120	118, 18, 119	syl2anr 495	. . . . . . . . . . . . . . . . . . . 20 $/\$
121	120	biimpa 501	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
122		elfzle2 12345	. . . . . . . . . . . . . . . . . . 19
123	121, 122	nsyl 135	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
124		disjsn 4246	. . . . . . . . . . . . . . . . . 18
125	123, 124	sylibr 224	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
126	118	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
127	18	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
128	50	nnred 11035	. . . . . . . . . . . . . . . . . . . . . 22
129	128	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
130		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
131	19	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
132	126, 127, 129, 130, 131	lttrd 10198	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
133		ltnle 10117	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
134	118, 128, 133	syl2anr 495	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	134	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136	132, 135	mpbid 222	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
137		elfzle2 12345	. . . . . . . . . . . . . . . . . . 19
138	136, 137	nsyl 135	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
139		disjsn 4246	. . . . . . . . . . . . . . . . . 18
140	138, 139	sylibr 224	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
141	125, 140	uneq12d 3768	. . . . . . . . . . . . . . . 16 $/\$ $/\$
142		df-pr 4180	. . . . . . . . . . . . . . . . . 18
143	142	ineq2i 3811	. . . . . . . . . . . . . . . . 17
144		indi 3873	. . . . . . . . . . . . . . . . 17
145	143, 144	eqtr2i 2645	. . . . . . . . . . . . . . . 16
146		un0 3967	. . . . . . . . . . . . . . . 16
147	141, 145, 146	3eqtr3g 2679	. . . . . . . . . . . . . . 15 $/\$ $/\$
148	116, 147	syl5eq 2668	. . . . . . . . . . . . . 14 $/\$ $/\$
149		fnimadisj 6012	. . . . . . . . . . . . . 14 $/\$
150	115, 148, 149	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$
151	39	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
152		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . 20
153		peano2uz 11741	. . . . . . . . . . . . . . . . . . . 20
154	152, 153	syl 17	. . . . . . . . . . . . . . . . . . 19
155	154	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$
156	151, 155	eqeltrrd 2702	. . . . . . . . . . . . . . . . 17 $/\$
157		fzss2 12381	. . . . . . . . . . . . . . . . 17
158		reldisj 4020	. . . . . . . . . . . . . . . . 17 $\$
159	156, 157, 158	3syl 18	. . . . . . . . . . . . . . . 16 $/\$ $\$
160	159	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
161	147, 160	mpbid 222	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
162		resiima 5480	. . . . . . . . . . . . . 14 $\$ $\$
163	161, 162	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
164	150, 163	uneq12d 3768	. . . . . . . . . . . 12 $/\$ $/\$ $\$
165		imaundir 5546	. . . . . . . . . . . 12 $\$ $\$
166		uncom 3757	. . . . . . . . . . . . 13
167		un0 3967	. . . . . . . . . . . . 13
168	166, 167	eqtr2i 2645	. . . . . . . . . . . 12
169	164, 165, 168	3eqtr4g 2681	. . . . . . . . . . 11 $/\$ $/\$ $\$
170	169	imaeq2d 5466	. . . . . . . . . 10 $/\$ $/\$ $\$
171	112, 170	syl5eq 2668	. . . . . . . . 9 $/\$ $/\$ $\$
172	171	xpeq1d 5138	. . . . . . . 8 $/\$ $/\$ $\$
173		imaco 5640	. . . . . . . . . 10 $\$ $\$
174		imaundir 5546	. . . . . . . . . . . . 13 $\$ $\$
175		imassrn 5477	. . . . . . . . . . . . . . . . 17
176	175	a1i 11	. . . . . . . . . . . . . . . 16 $/\$ $/\$
177		fnima 6010	. . . . . . . . . . . . . . . . . . 19
178	26, 113, 177	3syl 18	. . . . . . . . . . . . . . . . . 18
179	178	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
180		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . 22
181		zltp1le 11427	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
182	180, 57, 181	syl2anr 495	. . . . . . . . . . . . . . . . . . . . 21 $/\$
183	182	biimpa 501	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
184	18, 52, 56	ltled 10185	. . . . . . . . . . . . . . . . . . . . 21
185	184	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
186	57	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
187		nn0p1nn 11332	. . . . . . . . . . . . . . . . . . . . . . . . 25
188	117, 187	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
189	188	nnzd 11481	. . . . . . . . . . . . . . . . . . . . . . 23
190	189	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
191	40	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
192		elfz 12332	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
193	186, 190, 191, 192	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
194	193	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
195	183, 185, 194	mpbir2and 957	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
196		1red 10055	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
197		ltle 10126	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
198	118, 18, 197	syl2anr 495	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
199	198	imp 445	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
200	126, 127, 196, 199	leadd1dd 10641	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
201	60	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
202	57	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . 23
203	202	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
204		elfz 12332	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
205	203, 190, 191, 204	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
206	205	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
207	200, 201, 206	mpbir2and 957	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
208		prssi 4353	. . . . . . . . . . . . . . . . . . 19 $/\$
209	195, 207, 208	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
210		imass2 5501	. . . . . . . . . . . . . . . . . 18
211	209, 210	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
212	179, 211	eqsstr3d 3640	. . . . . . . . . . . . . . . 16 $/\$ $/\$
213	176, 212	eqssd 3620	. . . . . . . . . . . . . . 15 $/\$ $/\$
214		f1ofo 6144	. . . . . . . . . . . . . . . . . 18
215		forn 6118	. . . . . . . . . . . . . . . . . 18
216	26, 214, 215	3syl 18	. . . . . . . . . . . . . . . . 17
217	216, 27	syl6eq 2672	. . . . . . . . . . . . . . . 16
218	217	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$
219	213, 218	eqtrd 2656	. . . . . . . . . . . . . 14 $/\$ $/\$
220		undif 4049	. . . . . . . . . . . . . . . . 17 $\$
221	209, 220	sylib 208	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
222	221	imaeq2d 5466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$ $\$
223		fnresi 6008	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
224		incom 3805	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
225	224, 32	eqtri 2644	. . . . . . . . . . . . . . . . . . 19 $\$
226		fnimadisj 6012	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $/\$ $\$ $\$
227	223, 225, 226	mp2an 708	. . . . . . . . . . . . . . . . . 18 $\$
228	227	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
229		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . 22
230	188, 229	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . 21
231		fzss1 12380	. . . . . . . . . . . . . . . . . . . . 21
232	230, 231	syl 17	. . . . . . . . . . . . . . . . . . . 20
233	232	ssdifd 3746	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
234		resiima 5480	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $\$ $\$
235	233, 234	syl 17	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
236	235	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$ $\$
237	228, 236	uneq12d 3768	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$ $\$ $\$
238		imaundi 5545	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$ $\$
239		uncom 3757	. . . . . . . . . . . . . . . . 17 $\$ $\$
240		un0 3967	. . . . . . . . . . . . . . . . 17 $\$ $\$
241	239, 240	eqtr2i 2645	. . . . . . . . . . . . . . . 16 $\$ $\$
242	237, 238, 241	3eqtr4g 2681	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$ $\$
243	222, 242	eqtr3d 2658	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
244	219, 243	uneq12d 3768	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
245	174, 244	syl5eq 2668	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
246	245, 221	eqtrd 2656	. . . . . . . . . . 11 $/\$ $/\$ $\$
247	246	imaeq2d 5466	. . . . . . . . . 10 $/\$ $/\$ $\$
248	173, 247	syl5eq 2668	. . . . . . . . 9 $/\$ $/\$ $\$
249	248	xpeq1d 5138	. . . . . . . 8 $/\$ $/\$ $\$
250	172, 249	uneq12d 3768	. . . . . . 7 $/\$ $/\$ $\$ $\$
251	250	oveq2d 6666	. . . . . 6 $/\$ $/\$ $\$ $\$
252		iftrue 4092	. . . . . . . . 9
253	252	csbeq1d 3540	. . . . . . . 8 $\$ $\$ $\$ $\$
254		vex 3203	. . . . . . . . 9
255		oveq2 6658	. . . . . . . . . . . . 13
256	255	imaeq2d 5466	. . . . . . . . . . . 12 $\$ $\$
257	256	xpeq1d 5138	. . . . . . . . . . 11 $\$ $\$
258		oveq1 6657	. . . . . . . . . . . . . 14
259	258	oveq1d 6665	. . . . . . . . . . . . 13
260	259	imaeq2d 5466	. . . . . . . . . . . 12 $\$ $\$
261	260	xpeq1d 5138	. . . . . . . . . . 11 $\$ $\$
262	257, 261	uneq12d 3768	. . . . . . . . . 10 $\$ $\$ $\$ $\$
263	262	oveq2d 6666	. . . . . . . . 9 $\$ $\$ $\$ $\$
264	254, 263	csbie 3559	. . . . . . . 8 $\$ $\$ $\$ $\$
265	253, 264	syl6eq 2672	. . . . . . 7 $\$ $\$ $\$ $\$
266	265	adantl 482	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$ $\$
267	252	csbeq1d 3540	. . . . . . . 8
268	255	imaeq2d 5466	. . . . . . . . . . . 12
269	268	xpeq1d 5138	. . . . . . . . . . 11
270	259	imaeq2d 5466	. . . . . . . . . . . 12
271	270	xpeq1d 5138	. . . . . . . . . . 11
272	269, 271	uneq12d 3768	. . . . . . . . . 10
273	272	oveq2d 6666	. . . . . . . . 9
274	254, 273	csbie 3559	. . . . . . . 8
275	267, 274	syl6eq 2672	. . . . . . 7
276	275	adantl 482	. . . . . 6 $/\$ $/\$
277	251, 266, 276	3eqtr4d 2666	. . . . 5 $/\$ $/\$ $\$ $\$
278		lenlt 10116	. . . . . . . . . 10 $/\$
279	18, 118, 278	syl2an 494	. . . . . . . . 9 $/\$
280	279	biimpar 502	. . . . . . . 8 $/\$ $/\$
281		imaco 5640	. . . . . . . . . . 11 $\$ $\$
282		imaundir 5546	. . . . . . . . . . . . . 14 $\$ $\$
283		imassrn 5477	. . . . . . . . . . . . . . . . . 18
284	283	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
285	178	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
286	17	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
287	18	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
288	118	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
289	188	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . 23
290	289	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
291		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
292	118	lep1d 10955	. . . . . . . . . . . . . . . . . . . . . . 23
293	292	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
294	287, 288, 290, 291, 293	letrd 10194	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
295		fznn 12408	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
296	189, 295	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
297	296	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
298	286, 294, 297	mpbir2and 957	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
299	50	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
300		1red 10055	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
301	287, 288, 300, 291	leadd1dd 10641	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
302		fznn 12408	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
303	189, 302	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
304	303	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
305	299, 301, 304	mpbir2and 957	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
306		prssi 4353	. . . . . . . . . . . . . . . . . . . 20 $/\$
307	298, 305, 306	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
308		imass2 5501	. . . . . . . . . . . . . . . . . . 19
309	307, 308	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
310	285, 309	eqsstr3d 3640	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
311	284, 310	eqssd 3620	. . . . . . . . . . . . . . . 16 $/\$ $/\$
312	217	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$
313	311, 312	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ $/\$
314		undif 4049	. . . . . . . . . . . . . . . . . 18 $\$
315	307, 314	sylib 208	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
316	315	imaeq2d 5466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$ $\$
317	227	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$
318		eluzp1p1 11713	. . . . . . . . . . . . . . . . . . . . . . . . 25
319	152, 318	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
320	319	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
321	151, 320	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
322		fzss2 12381	. . . . . . . . . . . . . . . . . . . . . 22
323	321, 322	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$
324	323	ssdifd 3746	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$
325	324	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\$ $\$
326		resiima 5480	. . . . . . . . . . . . . . . . . . 19 $\$ $\$ $\$ $\$ $\$
327	325, 326	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$ $\$
328	317, 327	uneq12d 3768	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$ $\$ $\$
329		imaundi 5545	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$ $\$
330		uncom 3757	. . . . . . . . . . . . . . . . . 18 $\$ $\$
331		un0 3967	. . . . . . . . . . . . . . . . . 18 $\$ $\$
332	330, 331	eqtr2i 2645	. . . . . . . . . . . . . . . . 17 $\$ $\$
333	328, 329, 332	3eqtr4g 2681	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$ $\$
334	316, 333	eqtr3d 2658	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
335	313, 334	uneq12d 3768	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
336	282, 335	syl5eq 2668	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
337	336, 315	eqtrd 2656	. . . . . . . . . . . 12 $/\$ $/\$ $\$
338	337	imaeq2d 5466	. . . . . . . . . . 11 $/\$ $/\$ $\$
339	281, 338	syl5eq 2668	. . . . . . . . . 10 $/\$ $/\$ $\$
340	339	xpeq1d 5138	. . . . . . . . 9 $/\$ $/\$ $\$
341		imaco 5640	. . . . . . . . . . 11 $\$ $\$
342	114	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$
343		incom 3805	. . . . . . . . . . . . . . . 16
344	128	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
345	188	peano2nnd 11037	. . . . . . . . . . . . . . . . . . . . . . . 24
346	345	nnred 11035	. . . . . . . . . . . . . . . . . . . . . . 23
347	346	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
348	19	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
349	118	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . . . 25
350	349	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
351	287, 288, 290, 291, 350	lelttrd 10195	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
352	287, 290, 300, 351	ltadd1dd 10638	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
353	287, 344, 347, 348, 352	lttrd 10198	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
354		ltnle 10117	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
355	18, 346, 354	syl2an 494	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
356	355	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
357	353, 356	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
358		elfzle1 12344	. . . . . . . . . . . . . . . . . . . 20
359	357, 358	nsyl 135	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
360		disjsn 4246	. . . . . . . . . . . . . . . . . . 19
361	359, 360	sylibr 224	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
362		ltnle 10117	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
363	128, 346, 362	syl2an 494	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
364	363	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
365	352, 364	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
366		elfzle1 12344	. . . . . . . . . . . . . . . . . . . 20
367	365, 366	nsyl 135	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
368		disjsn 4246	. . . . . . . . . . . . . . . . . . 19
369	367, 368	sylibr 224	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
370	361, 369	uneq12d 3768	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
371	142	ineq2i 3811	. . . . . . . . . . . . . . . . . 18
372		indi 3873	. . . . . . . . . . . . . . . . . 18
373	371, 372	eqtr2i 2645	. . . . . . . . . . . . . . . . 17
374	370, 373, 146	3eqtr3g 2679	. . . . . . . . . . . . . . . 16 $/\$ $/\$
375	343, 374	syl5eq 2668	. . . . . . . . . . . . . . 15 $/\$ $/\$
376		fnimadisj 6012	. . . . . . . . . . . . . . 15 $/\$
377	342, 375, 376	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$
378	345, 229	syl6eleq 2711	. . . . . . . . . . . . . . . . . 18
379		fzss1 12380	. . . . . . . . . . . . . . . . . 18
380		reldisj 4020	. . . . . . . . . . . . . . . . . 18 $\$
381	378, 379, 380	3syl 18	. . . . . . . . . . . . . . . . 17 $\$
382	381	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
383	374, 382	mpbid 222	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
384		resiima 5480	. . . . . . . . . . . . . . 15 $\$ $\$
385	383, 384	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
386	377, 385	uneq12d 3768	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
387		imaundir 5546	. . . . . . . . . . . . 13 $\$ $\$
388		uncom 3757	. . . . . . . . . . . . . 14
389		un0 3967	. . . . . . . . . . . . . 14
390	388, 389	eqtr2i 2645	. . . . . . . . . . . . 13
391	386, 387, 390	3eqtr4g 2681	. . . . . . . . . . . 12 $/\$ $/\$ $\$
392	391	imaeq2d 5466	. . . . . . . . . . 11 $/\$ $/\$ $\$
393	341, 392	syl5eq 2668	. . . . . . . . . 10 $/\$ $/\$ $\$
394	393	xpeq1d 5138	. . . . . . . . 9 $/\$ $/\$ $\$
395	340, 394	uneq12d 3768	. . . . . . . 8 $/\$ $/\$ $\$ $\$
396	280, 395	syldan 487	. . . . . . 7 $/\$ $/\$ $\$ $\$
397	396	oveq2d 6666	. . . . . 6 $/\$ $/\$ $\$ $\$
398		iffalse 4095	. . . . . . . . 9
399	398	csbeq1d 3540	. . . . . . . 8 $\$ $\$ $\$ $\$
400		ovex 6678	. . . . . . . . 9
401		oveq2 6658	. . . . . . . . . . . . 13
402	401	imaeq2d 5466	. . . . . . . . . . . 12 $\$ $\$
403	402	xpeq1d 5138	. . . . . . . . . . 11 $\$ $\$
404		oveq1 6657	. . . . . . . . . . . . . 14
405	404	oveq1d 6665	. . . . . . . . . . . . 13
406	405	imaeq2d 5466	. . . . . . . . . . . 12 $\$ $\$
407	406	xpeq1d 5138	. . . . . . . . . . 11 $\$ $\$
408	403, 407	uneq12d 3768	. . . . . . . . . 10 $\$ $\$ $\$ $\$
409	408	oveq2d 6666	. . . . . . . . 9 $\$ $\$ $\$ $\$
410	400, 409	csbie 3559	. . . . . . . 8 $\$ $\$ $\$ $\$
411	399, 410	syl6eq 2672	. . . . . . 7 $\$ $\$ $\$ $\$
412	411	adantl 482	. . . . . 6 $/\$ $/\$ $\$ $\$ $\$ $\$
413	398	csbeq1d 3540	. . . . . . . 8
414	401	imaeq2d 5466	. . . . . . . . . . . 12
415	414	xpeq1d 5138	. . . . . . . . . . 11
416	405	imaeq2d 5466	. . . . . . . . . . . 12
417	416	xpeq1d 5138	. . . . . . . . . . 11
418	415, 417	uneq12d 3768	. . . . . . . . . 10
419	418	oveq2d 6666	. . . . . . . . 9
420	400, 419	csbie 3559	. . . . . . . 8
421	413, 420	syl6eq 2672	. . . . . . 7
422	421	adantl 482	. . . . . 6 $/\$ $/\$
423	397, 412, 422	3eqtr4d 2666	. . . . 5 $/\$ $/\$ $\$ $\$
424	277, 423	pm2.61dan 832	. . . 4 $/\$ $\$ $\$
425	424	mpteq2dva 4744	. . 3 $\$ $\$
426	111, 425	eqtr4d 2659	. 2 $\$ $\$
427		opex 4932	. . . . . . 7 $\$
428	427, 22	op1std 7178	. . . . . 6 $\$ $\$
429	427, 22	op2ndd 7179	. . . . . 6 $\$
430		breq2 4657	. . . . . . . . 9
431	430	ifbid 4108	. . . . . . . 8
432	431	csbeq1d 3540	. . . . . . 7
433		fvex 6201	. . . . . . . . . 10
434	433, 79	op1std 7178	. . . . . . . . 9 $\$
435	433, 79	op2ndd 7179	. . . . . . . . 9 $\$ $\$
436		id 22	. . . . . . . . . 10
437		imaeq1 5461	. . . . . . . . . . . 12 $\$ $\$
438	437	xpeq1d 5138	. . . . . . . . . . 11 $\$ $\$
439		imaeq1 5461	. . . . . . . . . . . 12 $\$ $\$
440	439	xpeq1d 5138	. . . . . . . . . . 11 $\$ $\$
441	438, 440	uneq12d 3768	. . . . . . . . . 10 $\$ $\$ $\$
442	436, 441	oveqan12d 6669	. . . . . . . . 9 $/\$ $\$ $\$ $\$
443	434, 435, 442	syl2anc 693	. . . . . . . 8 $\$ $\$ $\$
444	443	csbeq2dv 3992	. . . . . . 7 $\$ $\$ $\$
445	432, 444	sylan9eqr 2678	. . . . . 6 $\$ $/\$ $\$ $\$
446	428, 429, 445	syl2anc 693	. . . . 5 $\$ $\$ $\$
447	446	mpteq2dv 4745	. . . 4 $\$ $\$ $\$
448	447	eqeq2d 2632	. . 3 $\$ $\$ $\$
449	448, 3	elrab2 3366	. 2 $\$ $\$ ..^ $/\$ $\$ $\$
450	91, 426, 449	sylanbrc 698	1 $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384

wceq 1483

wcel 1990

cab 2608

wne 2794

crab 2916

cvv 3200

csb 3533 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cif 4086

csn 4177

cpr 4179

cop 4183 class class class wbr 4653

cmpt 4729

cid 5023

cxp 5112

crn 5115

cres 5116

cima 5117

ccom 5118

wfn 5883

wf 5884

wfo 5886

wf1o 5887

cfv 5888 (class class class)co 6650

cof 6895

c1st 7166

c2nd 7167

cmap 7857

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-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-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-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 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

This theorem is referenced by: poimirlem22 33431

W3C validator