poimirlem12 - Mathbox for Brendan Leahy

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

Theorem poimirlem12 32016

Description: Lemma for poimir 32037 connecting walks that could yield from a given cube a given face opposite the final vertex of the walk. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem22.s	..^
poimirlem22.1
poimirlem12.2
poimirlem12.3
poimirlem12.4
poimirlem12.5
poimirlem12.6

**Assertion**
Ref	Expression
poimirlem12

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

**Proof of Theorem poimirlem12**
Step	Hyp	Ref	Expression
1		eldif 3400	. . . . . . 7 $\$ $/\$
2		imassrn 5185	. . . . . . . . . . . 12
3		poimirlem12.2	. . . . . . . . . . . . . . . 16
4		elrabi 3181	. . . . . . . . . . . . . . . . 17 ..^ ..^
5		poimirlem22.s	. . . . . . . . . . . . . . . . 17 ..^
6	4, 5	eleq2s 2567	. . . . . . . . . . . . . . . 16 ..^
7		xp1st 6842	. . . . . . . . . . . . . . . 16 ..^ ..^
8	3, 6, 7	3syl 18	. . . . . . . . . . . . . . 15 ..^
9		xp2nd 6843	. . . . . . . . . . . . . . 15 ..^
10	8, 9	syl 17	. . . . . . . . . . . . . 14
11		fvex 5889	. . . . . . . . . . . . . . 15
12		f1oeq1 5818	. . . . . . . . . . . . . . 15
13	11, 12	elab 3173	. . . . . . . . . . . . . 14
14	10, 13	sylib 201	. . . . . . . . . . . . 13
15		f1of 5828	. . . . . . . . . . . . 13
16		frn 5747	. . . . . . . . . . . . 13
17	14, 15, 16	3syl 18	. . . . . . . . . . . 12
18	2, 17	syl5ss 3429	. . . . . . . . . . 11
19		poimirlem12.4	. . . . . . . . . . . . . . 15
20		elrabi 3181	. . . . . . . . . . . . . . . 16 ..^ ..^
21	20, 5	eleq2s 2567	. . . . . . . . . . . . . . 15 ..^
22		xp1st 6842	. . . . . . . . . . . . . . 15 ..^ ..^
23	19, 21, 22	3syl 18	. . . . . . . . . . . . . 14 ..^
24		xp2nd 6843	. . . . . . . . . . . . . 14 ..^
25	23, 24	syl 17	. . . . . . . . . . . . 13
26		fvex 5889	. . . . . . . . . . . . . 14
27		f1oeq1 5818	. . . . . . . . . . . . . 14
28	26, 27	elab 3173	. . . . . . . . . . . . 13
29	25, 28	sylib 201	. . . . . . . . . . . 12
30		f1ofo 5835	. . . . . . . . . . . 12
31		foima 5811	. . . . . . . . . . . 12
32	29, 30, 31	3syl 18	. . . . . . . . . . 11
33	18, 32	sseqtr4d 3455	. . . . . . . . . 10
34	33	ssdifd 3558	. . . . . . . . 9 $\$ $\$
35		dff1o3 5834	. . . . . . . . . . . 12 $/\$
36	35	simprbi 471	. . . . . . . . . . 11
37		imadif 5668	. . . . . . . . . . 11 $\$ $\$
38	29, 36, 37	3syl 18	. . . . . . . . . 10 $\$ $\$
39		difun2 3838	. . . . . . . . . . . 12 $\$ $\$
40		poimirlem12.6	. . . . . . . . . . . . . . . . 17
41		elfznn0 11913	. . . . . . . . . . . . . . . . 17
42		nn0p1nn 10933	. . . . . . . . . . . . . . . . 17
43	40, 41, 42	3syl 18	. . . . . . . . . . . . . . . 16
44		nnuz 11218	. . . . . . . . . . . . . . . 16
45	43, 44	syl6eleq 2559	. . . . . . . . . . . . . . 15
46		poimir.0	. . . . . . . . . . . . . . . . . 18
47	46	nncnd 10647	. . . . . . . . . . . . . . . . 17
48		npcan1 10065	. . . . . . . . . . . . . . . . 17
49	47, 48	syl 17	. . . . . . . . . . . . . . . 16
50		elfzuz3 11823	. . . . . . . . . . . . . . . . 17
51		peano2uz 11235	. . . . . . . . . . . . . . . . 17
52	40, 50, 51	3syl 18	. . . . . . . . . . . . . . . 16
53	49, 52	eqeltrrd 2550	. . . . . . . . . . . . . . 15
54		fzsplit2 11850	. . . . . . . . . . . . . . 15 $/\$
55	45, 53, 54	syl2anc 673	. . . . . . . . . . . . . 14
56		uncom 3569	. . . . . . . . . . . . . 14
57	55, 56	syl6eq 2521	. . . . . . . . . . . . 13
58	57	difeq1d 3539	. . . . . . . . . . . 12 $\$ $\$
59		incom 3616	. . . . . . . . . . . . . 14
60	40, 41	syl 17	. . . . . . . . . . . . . . . . 17
61	60	nn0red 10950	. . . . . . . . . . . . . . . 16
62	61	ltp1d 10559	. . . . . . . . . . . . . . 15
63		fzdisj 11852	. . . . . . . . . . . . . . 15
64	62, 63	syl 17	. . . . . . . . . . . . . 14
65	59, 64	syl5eq 2517	. . . . . . . . . . . . 13
66		disj3 3813	. . . . . . . . . . . . 13 $\$
67	65, 66	sylib 201	. . . . . . . . . . . 12 $\$
68	39, 58, 67	3eqtr4a 2531	. . . . . . . . . . 11 $\$
69	68	imaeq2d 5174	. . . . . . . . . 10 $\$
70	38, 69	eqtr3d 2507	. . . . . . . . 9 $\$
71	34, 70	sseqtrd 3454	. . . . . . . 8 $\$
72	71	sselda 3418	. . . . . . 7 $/\$ $\$
73	1, 72	sylan2br 484	. . . . . 6 $/\$ $/\$
74		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
75	74	breq2d 4407	. . . . . . . . . . . . . . . . . 18
76	75	ifbid 3894	. . . . . . . . . . . . . . . . 17
77	76	csbeq1d 3356	. . . . . . . . . . . . . . . 16
78		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
79	78	fveq2d 5883	. . . . . . . . . . . . . . . . . 18
80	78	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21
81	80	imaeq1d 5173	. . . . . . . . . . . . . . . . . . . 20
82	81	xpeq1d 4862	. . . . . . . . . . . . . . . . . . 19
83	80	imaeq1d 5173	. . . . . . . . . . . . . . . . . . . 20
84	83	xpeq1d 4862	. . . . . . . . . . . . . . . . . . 19
85	82, 84	uneq12d 3580	. . . . . . . . . . . . . . . . . 18
86	79, 85	oveq12d 6326	. . . . . . . . . . . . . . . . 17
87	86	csbeq2dv 3785	. . . . . . . . . . . . . . . 16
88	77, 87	eqtrd 2505	. . . . . . . . . . . . . . 15
89	88	mpteq2dv 4483	. . . . . . . . . . . . . 14
90	89	eqeq2d 2481	. . . . . . . . . . . . 13
91	90, 5	elrab2 3186	. . . . . . . . . . . 12 ..^ $/\$
92	91	simprbi 471	. . . . . . . . . . 11
93	19, 92	syl 17	. . . . . . . . . 10
94		breq1 4398	. . . . . . . . . . . . . 14
95		id 22	. . . . . . . . . . . . . 14
96	94, 95	ifbieq1d 3895	. . . . . . . . . . . . 13
97	46	nnred 10646	. . . . . . . . . . . . . . . . 17
98		peano2rem 9961	. . . . . . . . . . . . . . . . 17
99	97, 98	syl 17	. . . . . . . . . . . . . . . 16
100		elfzle2 11829	. . . . . . . . . . . . . . . . 17
101	40, 100	syl 17	. . . . . . . . . . . . . . . 16
102	97	ltm1d 10561	. . . . . . . . . . . . . . . 16
103	61, 99, 97, 101, 102	lelttrd 9810	. . . . . . . . . . . . . . 15
104		poimirlem12.5	. . . . . . . . . . . . . . 15
105	103, 104	breqtrrd 4422	. . . . . . . . . . . . . 14
106	105	iftrued 3880	. . . . . . . . . . . . 13
107	96, 106	sylan9eqr 2527	. . . . . . . . . . . 12 $/\$
108	107	csbeq1d 3356	. . . . . . . . . . 11 $/\$
109		oveq2 6316	. . . . . . . . . . . . . . . . . 18
110	109	imaeq2d 5174	. . . . . . . . . . . . . . . . 17
111	110	xpeq1d 4862	. . . . . . . . . . . . . . . 16
112		oveq1 6315	. . . . . . . . . . . . . . . . . . 19
113	112	oveq1d 6323	. . . . . . . . . . . . . . . . . 18
114	113	imaeq2d 5174	. . . . . . . . . . . . . . . . 17
115	114	xpeq1d 4862	. . . . . . . . . . . . . . . 16
116	111, 115	uneq12d 3580	. . . . . . . . . . . . . . 15
117	116	oveq2d 6324	. . . . . . . . . . . . . 14
118	117	adantl 473	. . . . . . . . . . . . 13 $/\$
119	40, 118	csbied 3376	. . . . . . . . . . . 12
120	119	adantr 472	. . . . . . . . . . 11 $/\$
121	108, 120	eqtrd 2505	. . . . . . . . . 10 $/\$
122		ovex 6336	. . . . . . . . . . 11
123	122	a1i 11	. . . . . . . . . 10
124	93, 121, 40, 123	fvmptd 5969	. . . . . . . . 9
125	124	fveq1d 5881	. . . . . . . 8
126	125	adantr 472	. . . . . . 7 $/\$
127		imassrn 5185	. . . . . . . . . 10
128		f1of 5828	. . . . . . . . . . 11
129		frn 5747	. . . . . . . . . . 11
130	29, 128, 129	3syl 18	. . . . . . . . . 10
131	127, 130	syl5ss 3429	. . . . . . . . 9
132	131	sselda 3418	. . . . . . . 8 $/\$
133		xp1st 6842	. . . . . . . . . . 11 ..^ ..^
134		elmapfn 7512	. . . . . . . . . . 11 ..^
135	23, 133, 134	3syl 18	. . . . . . . . . 10
136	135	adantr 472	. . . . . . . . 9 $/\$
137		1ex 9656	. . . . . . . . . . . . . 14
138		fnconstg 5784	. . . . . . . . . . . . . 14
139	137, 138	ax-mp 5	. . . . . . . . . . . . 13
140		c0ex 9655	. . . . . . . . . . . . . 14
141		fnconstg 5784	. . . . . . . . . . . . . 14
142	140, 141	ax-mp 5	. . . . . . . . . . . . 13
143	139, 142	pm3.2i 462	. . . . . . . . . . . 12 $/\$
144		imain 5669	. . . . . . . . . . . . . 14
145	29, 36, 144	3syl 18	. . . . . . . . . . . . 13
146	64	imaeq2d 5174	. . . . . . . . . . . . . 14
147		ima0 5189	. . . . . . . . . . . . . 14
148	146, 147	syl6eq 2521	. . . . . . . . . . . . 13
149	145, 148	eqtr3d 2507	. . . . . . . . . . . 12
150		fnun 5692	. . . . . . . . . . . 12 $/\$ $/\$
151	143, 149, 150	sylancr 676	. . . . . . . . . . 11
152		imaundi 5254	. . . . . . . . . . . . 13
153	55	imaeq2d 5174	. . . . . . . . . . . . . 14
154	153, 32	eqtr3d 2507	. . . . . . . . . . . . 13
155	152, 154	syl5eqr 2519	. . . . . . . . . . . 12
156	155	fneq2d 5677	. . . . . . . . . . 11
157	151, 156	mpbid 215	. . . . . . . . . 10
158	157	adantr 472	. . . . . . . . 9 $/\$
159		ovex 6336	. . . . . . . . . 10
160	159	a1i 11	. . . . . . . . 9 $/\$
161		inidm 3632	. . . . . . . . 9
162		eqidd 2472	. . . . . . . . 9 $/\$ $/\$
163		fvun2 5952	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
164	139, 142, 163	mp3an12 1380	. . . . . . . . . . . 12 $/\$
165	149, 164	sylan 479	. . . . . . . . . . 11 $/\$
166	140	fvconst2 6136	. . . . . . . . . . . 12
167	166	adantl 473	. . . . . . . . . . 11 $/\$
168	165, 167	eqtrd 2505	. . . . . . . . . 10 $/\$
169	168	adantr 472	. . . . . . . . 9 $/\$ $/\$
170	136, 158, 160, 160, 161, 162, 169	ofval 6559	. . . . . . . 8 $/\$ $/\$
171	132, 170	mpdan 681	. . . . . . 7 $/\$
172		elmapi 7511	. . . . . . . . . . . . 13 ..^ ..^
173	23, 133, 172	3syl 18	. . . . . . . . . . . 12 ..^
174	173	ffvelrnda 6037	. . . . . . . . . . 11 $/\$ ..^
175		elfzonn0 11988	. . . . . . . . . . 11 ..^
176	174, 175	syl 17	. . . . . . . . . 10 $/\$
177	176	nn0cnd 10951	. . . . . . . . 9 $/\$
178	177	addid1d 9851	. . . . . . . 8 $/\$
179	132, 178	syldan 478	. . . . . . 7 $/\$
180	126, 171, 179	3eqtrd 2509	. . . . . 6 $/\$
181	73, 180	syldan 478	. . . . 5 $/\$ $/\$
182		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
183	182	breq2d 4407	. . . . . . . . . . . . . . . . . 18
184	183	ifbid 3894	. . . . . . . . . . . . . . . . 17
185	184	csbeq1d 3356	. . . . . . . . . . . . . . . 16
186		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
187	186	fveq2d 5883	. . . . . . . . . . . . . . . . . 18
188	186	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21
189	188	imaeq1d 5173	. . . . . . . . . . . . . . . . . . . 20
190	189	xpeq1d 4862	. . . . . . . . . . . . . . . . . . 19
191	188	imaeq1d 5173	. . . . . . . . . . . . . . . . . . . 20
192	191	xpeq1d 4862	. . . . . . . . . . . . . . . . . . 19
193	190, 192	uneq12d 3580	. . . . . . . . . . . . . . . . . 18
194	187, 193	oveq12d 6326	. . . . . . . . . . . . . . . . 17
195	194	csbeq2dv 3785	. . . . . . . . . . . . . . . 16
196	185, 195	eqtrd 2505	. . . . . . . . . . . . . . 15
197	196	mpteq2dv 4483	. . . . . . . . . . . . . 14
198	197	eqeq2d 2481	. . . . . . . . . . . . 13
199	198, 5	elrab2 3186	. . . . . . . . . . . 12 ..^ $/\$
200	199	simprbi 471	. . . . . . . . . . 11
201	3, 200	syl 17	. . . . . . . . . 10
202		breq1 4398	. . . . . . . . . . . . . 14
203	202, 95	ifbieq1d 3895	. . . . . . . . . . . . 13
204		poimirlem12.3	. . . . . . . . . . . . . . 15
205	103, 204	breqtrrd 4422	. . . . . . . . . . . . . 14
206	205	iftrued 3880	. . . . . . . . . . . . 13
207	203, 206	sylan9eqr 2527	. . . . . . . . . . . 12 $/\$
208	207	csbeq1d 3356	. . . . . . . . . . 11 $/\$
209	109	imaeq2d 5174	. . . . . . . . . . . . . . . . 17
210	209	xpeq1d 4862	. . . . . . . . . . . . . . . 16
211	113	imaeq2d 5174	. . . . . . . . . . . . . . . . 17
212	211	xpeq1d 4862	. . . . . . . . . . . . . . . 16
213	210, 212	uneq12d 3580	. . . . . . . . . . . . . . 15
214	213	oveq2d 6324	. . . . . . . . . . . . . 14
215	214	adantl 473	. . . . . . . . . . . . 13 $/\$
216	40, 215	csbied 3376	. . . . . . . . . . . 12
217	216	adantr 472	. . . . . . . . . . 11 $/\$
218	208, 217	eqtrd 2505	. . . . . . . . . 10 $/\$
219		ovex 6336	. . . . . . . . . . 11
220	219	a1i 11	. . . . . . . . . 10
221	201, 218, 40, 220	fvmptd 5969	. . . . . . . . 9
222	221	fveq1d 5881	. . . . . . . 8
223	222	adantr 472	. . . . . . 7 $/\$
224	18	sselda 3418	. . . . . . . 8 $/\$
225		xp1st 6842	. . . . . . . . . . 11 ..^ ..^
226		elmapfn 7512	. . . . . . . . . . 11 ..^
227	8, 225, 226	3syl 18	. . . . . . . . . 10
228	227	adantr 472	. . . . . . . . 9 $/\$
229		fnconstg 5784	. . . . . . . . . . . . . 14
230	137, 229	ax-mp 5	. . . . . . . . . . . . 13
231		fnconstg 5784	. . . . . . . . . . . . . 14
232	140, 231	ax-mp 5	. . . . . . . . . . . . 13
233	230, 232	pm3.2i 462	. . . . . . . . . . . 12 $/\$
234		dff1o3 5834	. . . . . . . . . . . . . . 15 $/\$
235	234	simprbi 471	. . . . . . . . . . . . . 14
236		imain 5669	. . . . . . . . . . . . . 14
237	14, 235, 236	3syl 18	. . . . . . . . . . . . 13
238	64	imaeq2d 5174	. . . . . . . . . . . . . 14
239		ima0 5189	. . . . . . . . . . . . . 14
240	238, 239	syl6eq 2521	. . . . . . . . . . . . 13
241	237, 240	eqtr3d 2507	. . . . . . . . . . . 12
242		fnun 5692	. . . . . . . . . . . 12 $/\$ $/\$
243	233, 241, 242	sylancr 676	. . . . . . . . . . 11
244		imaundi 5254	. . . . . . . . . . . . 13
245	55	imaeq2d 5174	. . . . . . . . . . . . . 14
246		f1ofo 5835	. . . . . . . . . . . . . . 15
247		foima 5811	. . . . . . . . . . . . . . 15
248	14, 246, 247	3syl 18	. . . . . . . . . . . . . 14
249	245, 248	eqtr3d 2507	. . . . . . . . . . . . 13
250	244, 249	syl5eqr 2519	. . . . . . . . . . . 12
251	250	fneq2d 5677	. . . . . . . . . . 11
252	243, 251	mpbid 215	. . . . . . . . . 10
253	252	adantr 472	. . . . . . . . 9 $/\$