poimirlem12 - Mathbox for Brendan Leahy

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

Theorem poimirlem12 31872

Description: Lemma for poimir 31893 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 3447	. . . . . . 7 $\$ $/\$
2		imassrn 5196	. . . . . . . . . . . 12
3		poimirlem12.2	. . . . . . . . . . . . . . . 16
4		elrabi 3227	. . . . . . . . . . . . . . . . 17 ..^ ..^
5		poimirlem22.s	. . . . . . . . . . . . . . . . 17 ..^
6	4, 5	eleq2s 2531	. . . . . . . . . . . . . . . 16 ..^
7		xp1st 6835	. . . . . . . . . . . . . . . 16 ..^ ..^
8	3, 6, 7	3syl 18	. . . . . . . . . . . . . . 15 ..^
9		xp2nd 6836	. . . . . . . . . . . . . . 15 ..^
10	8, 9	syl 17	. . . . . . . . . . . . . 14
11		fvex 5889	. . . . . . . . . . . . . . 15
12		f1oeq1 5820	. . . . . . . . . . . . . . 15
13	11, 12	elab 3219	. . . . . . . . . . . . . 14
14	10, 13	sylib 200	. . . . . . . . . . . . 13
15		f1of 5829	. . . . . . . . . . . . 13
16		frn 5750	. . . . . . . . . . . . 13
17	14, 15, 16	3syl 18	. . . . . . . . . . . 12
18	2, 17	syl5ss 3476	. . . . . . . . . . 11
19		poimirlem12.4	. . . . . . . . . . . . . . 15
20		elrabi 3227	. . . . . . . . . . . . . . . 16 ..^ ..^
21	20, 5	eleq2s 2531	. . . . . . . . . . . . . . 15 ..^
22		xp1st 6835	. . . . . . . . . . . . . . 15 ..^ ..^
23	19, 21, 22	3syl 18	. . . . . . . . . . . . . 14 ..^
24		xp2nd 6836	. . . . . . . . . . . . . 14 ..^
25	23, 24	syl 17	. . . . . . . . . . . . 13
26		fvex 5889	. . . . . . . . . . . . . 14
27		f1oeq1 5820	. . . . . . . . . . . . . 14
28	26, 27	elab 3219	. . . . . . . . . . . . 13
29	25, 28	sylib 200	. . . . . . . . . . . 12
30		f1ofo 5836	. . . . . . . . . . . 12
31		foima 5813	. . . . . . . . . . . 12
32	29, 30, 31	3syl 18	. . . . . . . . . . 11
33	18, 32	sseqtr4d 3502	. . . . . . . . . 10
34	33	ssdifd 3602	. . . . . . . . 9 $\$ $\$
35		dff1o3 5835	. . . . . . . . . . . 12 $/\$
36	35	simprbi 466	. . . . . . . . . . 11
37		imadif 5674	. . . . . . . . . . 11 $\$ $\$
38	29, 36, 37	3syl 18	. . . . . . . . . 10 $\$ $\$
39		difun2 3876	. . . . . . . . . . . 12 $\$ $\$
40		poimirlem12.6	. . . . . . . . . . . . . . . . 17
41		elfznn0 11889	. . . . . . . . . . . . . . . . 17
42		nn0p1nn 10911	. . . . . . . . . . . . . . . . 17
43	40, 41, 42	3syl 18	. . . . . . . . . . . . . . . 16
44		nnuz 11196	. . . . . . . . . . . . . . . 16
45	43, 44	syl6eleq 2521	. . . . . . . . . . . . . . 15
46		poimir.0	. . . . . . . . . . . . . . . . . 18
47	46	nncnd 10627	. . . . . . . . . . . . . . . . 17
48		npcan1 10046	. . . . . . . . . . . . . . . . 17
49	47, 48	syl 17	. . . . . . . . . . . . . . . 16
50		elfzuz3 11799	. . . . . . . . . . . . . . . . 17
51		peano2uz 11214	. . . . . . . . . . . . . . . . 17
52	40, 50, 51	3syl 18	. . . . . . . . . . . . . . . 16
53	49, 52	eqeltrrd 2512	. . . . . . . . . . . . . . 15
54		fzsplit2 11826	. . . . . . . . . . . . . . 15 $/\$
55	45, 53, 54	syl2anc 666	. . . . . . . . . . . . . 14
56		uncom 3611	. . . . . . . . . . . . . 14
57	55, 56	syl6eq 2480	. . . . . . . . . . . . 13
58	57	difeq1d 3583	. . . . . . . . . . . 12 $\$ $\$
59		incom 3656	. . . . . . . . . . . . . 14
60	40, 41	syl 17	. . . . . . . . . . . . . . . . 17
61	60	nn0red 10928	. . . . . . . . . . . . . . . 16
62	61	ltp1d 10539	. . . . . . . . . . . . . . 15
63		fzdisj 11828	. . . . . . . . . . . . . . 15
64	62, 63	syl 17	. . . . . . . . . . . . . 14
65	59, 64	syl5eq 2476	. . . . . . . . . . . . 13
66		disj3 3838	. . . . . . . . . . . . 13 $\$
67	65, 66	sylib 200	. . . . . . . . . . . 12 $\$
68	39, 58, 67	3eqtr4a 2490	. . . . . . . . . . 11 $\$
69	68	imaeq2d 5185	. . . . . . . . . 10 $\$
70	38, 69	eqtr3d 2466	. . . . . . . . 9 $\$
71	34, 70	sseqtrd 3501	. . . . . . . 8 $\$
72	71	sselda 3465	. . . . . . 7 $/\$ $\$
73	1, 72	sylan2br 479	. . . . . 6 $/\$ $/\$
74		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
75	74	breq2d 4433	. . . . . . . . . . . . . . . . . 18
76	75	ifbid 3932	. . . . . . . . . . . . . . . . 17
77	76	csbeq1d 3403	. . . . . . . . . . . . . . . 16
78		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
79	78	fveq2d 5883	. . . . . . . . . . . . . . . . . 18
80	78	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21
81	80	imaeq1d 5184	. . . . . . . . . . . . . . . . . . . 20
82	81	xpeq1d 4874	. . . . . . . . . . . . . . . . . . 19
83	80	imaeq1d 5184	. . . . . . . . . . . . . . . . . . . 20
84	83	xpeq1d 4874	. . . . . . . . . . . . . . . . . . 19
85	82, 84	uneq12d 3622	. . . . . . . . . . . . . . . . . 18
86	79, 85	oveq12d 6321	. . . . . . . . . . . . . . . . 17
87	86	csbeq2dv 3810	. . . . . . . . . . . . . . . 16
88	77, 87	eqtrd 2464	. . . . . . . . . . . . . . 15
89	88	mpteq2dv 4509	. . . . . . . . . . . . . 14
90	89	eqeq2d 2437	. . . . . . . . . . . . 13
91	90, 5	elrab2 3232	. . . . . . . . . . . 12 ..^ $/\$
92	91	simprbi 466	. . . . . . . . . . 11
93	19, 92	syl 17	. . . . . . . . . 10
94		breq1 4424	. . . . . . . . . . . . . 14
95		id 23	. . . . . . . . . . . . . 14
96	94, 95	ifbieq1d 3933	. . . . . . . . . . . . 13
97	46	nnred 10626	. . . . . . . . . . . . . . . . 17
98		peano2rem 9943	. . . . . . . . . . . . . . . . 17
99	97, 98	syl 17	. . . . . . . . . . . . . . . 16
100		elfzle2 11805	. . . . . . . . . . . . . . . . 17
101	40, 100	syl 17	. . . . . . . . . . . . . . . 16
102	97	ltm1d 10541	. . . . . . . . . . . . . . . 16
103	61, 99, 97, 101, 102	lelttrd 9795	. . . . . . . . . . . . . . 15
104		poimirlem12.5	. . . . . . . . . . . . . . 15
105	103, 104	breqtrrd 4448	. . . . . . . . . . . . . 14
106	105	iftrued 3918	. . . . . . . . . . . . 13
107	96, 106	sylan9eqr 2486	. . . . . . . . . . . 12 $/\$
108	107	csbeq1d 3403	. . . . . . . . . . 11 $/\$
109		oveq2 6311	. . . . . . . . . . . . . . . . . 18
110	109	imaeq2d 5185	. . . . . . . . . . . . . . . . 17
111	110	xpeq1d 4874	. . . . . . . . . . . . . . . 16
112		oveq1 6310	. . . . . . . . . . . . . . . . . . 19
113	112	oveq1d 6318	. . . . . . . . . . . . . . . . . 18
114	113	imaeq2d 5185	. . . . . . . . . . . . . . . . 17
115	114	xpeq1d 4874	. . . . . . . . . . . . . . . 16
116	111, 115	uneq12d 3622	. . . . . . . . . . . . . . 15
117	116	oveq2d 6319	. . . . . . . . . . . . . 14
118	117	adantl 468	. . . . . . . . . . . . 13 $/\$
119	40, 118	csbied 3423	. . . . . . . . . . . 12
120	119	adantr 467	. . . . . . . . . . 11 $/\$
121	108, 120	eqtrd 2464	. . . . . . . . . 10 $/\$
122		ovex 6331	. . . . . . . . . . 11
123	122	a1i 11	. . . . . . . . . 10
124	93, 121, 40, 123	fvmptd 5968	. . . . . . . . 9
125	124	fveq1d 5881	. . . . . . . 8
126	125	adantr 467	. . . . . . 7 $/\$
127		imassrn 5196	. . . . . . . . . 10
128		f1of 5829	. . . . . . . . . . 11
129		frn 5750	. . . . . . . . . . 11
130	29, 128, 129	3syl 18	. . . . . . . . . 10
131	127, 130	syl5ss 3476	. . . . . . . . 9
132	131	sselda 3465	. . . . . . . 8 $/\$
133		xp1st 6835	. . . . . . . . . . 11 ..^ ..^
134		elmapfn 7500	. . . . . . . . . . 11 ..^
135	23, 133, 134	3syl 18	. . . . . . . . . 10
136	135	adantr 467	. . . . . . . . 9 $/\$
137		1ex 9640	. . . . . . . . . . . . . 14
138		fnconstg 5786	. . . . . . . . . . . . . 14
139	137, 138	ax-mp 5	. . . . . . . . . . . . 13
140		c0ex 9639	. . . . . . . . . . . . . 14
141		fnconstg 5786	. . . . . . . . . . . . . 14
142	140, 141	ax-mp 5	. . . . . . . . . . . . 13
143	139, 142	pm3.2i 457	. . . . . . . . . . . 12 $/\$
144		imain 5675	. . . . . . . . . . . . . 14
145	29, 36, 144	3syl 18	. . . . . . . . . . . . 13
146	64	imaeq2d 5185	. . . . . . . . . . . . . 14
147		ima0 5200	. . . . . . . . . . . . . 14
148	146, 147	syl6eq 2480	. . . . . . . . . . . . 13
149	145, 148	eqtr3d 2466	. . . . . . . . . . . 12
150		fnun 5698	. . . . . . . . . . . 12 $/\$ $/\$
151	143, 149, 150	sylancr 668	. . . . . . . . . . 11
152		imaundi 5265	. . . . . . . . . . . . 13
153	55	imaeq2d 5185	. . . . . . . . . . . . . 14
154	153, 32	eqtr3d 2466	. . . . . . . . . . . . 13
155	152, 154	syl5eqr 2478	. . . . . . . . . . . 12
156	155	fneq2d 5683	. . . . . . . . . . 11
157	151, 156	mpbid 214	. . . . . . . . . 10
158	157	adantr 467	. . . . . . . . 9 $/\$
159		ovex 6331	. . . . . . . . . 10
160	159	a1i 11	. . . . . . . . 9 $/\$
161		inidm 3672	. . . . . . . . 9
162		eqidd 2424	. . . . . . . . 9 $/\$ $/\$
163		fvun2 5951	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
164	139, 142, 163	mp3an12 1351	. . . . . . . . . . . 12 $/\$
165	149, 164	sylan 474	. . . . . . . . . . 11 $/\$
166	140	fvconst2 6133	. . . . . . . . . . . 12
167	166	adantl 468	. . . . . . . . . . 11 $/\$
168	165, 167	eqtrd 2464	. . . . . . . . . 10 $/\$
169	168	adantr 467	. . . . . . . . 9 $/\$ $/\$
170	136, 158, 160, 160, 161, 162, 169	ofval 6552	. . . . . . . 8 $/\$ $/\$
171	132, 170	mpdan 673	. . . . . . 7 $/\$
172		elmapi 7499	. . . . . . . . . . . . 13 ..^ ..^
173	23, 133, 172	3syl 18	. . . . . . . . . . . 12 ..^
174	173	ffvelrnda 6035	. . . . . . . . . . 11 $/\$ ..^
175		elfzonn0 11962	. . . . . . . . . . 11 ..^
176	174, 175	syl 17	. . . . . . . . . 10 $/\$
177	176	nn0cnd 10929	. . . . . . . . 9 $/\$
178	177	addid1d 9835	. . . . . . . 8 $/\$
179	132, 178	syldan 473	. . . . . . 7 $/\$
180	126, 171, 179	3eqtrd 2468	. . . . . 6 $/\$
181	73, 180	syldan 473	. . . . 5 $/\$ $/\$
182		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
183	182	breq2d 4433	. . . . . . . . . . . . . . . . . 18
184	183	ifbid 3932	. . . . . . . . . . . . . . . . 17
185	184	csbeq1d 3403	. . . . . . . . . . . . . . . 16
186		fveq2 5879	. . . . . . . . . . . . . . . . . . 19
187	186	fveq2d 5883	. . . . . . . . . . . . . . . . . 18
188	186	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21
189	188	imaeq1d 5184	. . . . . . . . . . . . . . . . . . . 20
190	189	xpeq1d 4874	. . . . . . . . . . . . . . . . . . 19
191	188	imaeq1d 5184	. . . . . . . . . . . . . . . . . . . 20
192	191	xpeq1d 4874	. . . . . . . . . . . . . . . . . . 19
193	190, 192	uneq12d 3622	. . . . . . . . . . . . . . . . . 18
194	187, 193	oveq12d 6321	. . . . . . . . . . . . . . . . 17
195	194	csbeq2dv 3810	. . . . . . . . . . . . . . . 16
196	185, 195	eqtrd 2464	. . . . . . . . . . . . . . 15
197	196	mpteq2dv 4509	. . . . . . . . . . . . . 14
198	197	eqeq2d 2437	. . . . . . . . . . . . 13
199	198, 5	elrab2 3232	. . . . . . . . . . . 12 ..^ $/\$
200	199	simprbi 466	. . . . . . . . . . 11
201	3, 200	syl 17	. . . . . . . . . 10
202		breq1 4424	. . . . . . . . . . . . . 14
203	202, 95	ifbieq1d 3933	. . . . . . . . . . . . 13
204		poimirlem12.3	. . . . . . . . . . . . . . 15
205	103, 204	breqtrrd 4448	. . . . . . . . . . . . . 14
206	205	iftrued 3918	. . . . . . . . . . . . 13
207	203, 206	sylan9eqr 2486	. . . . . . . . . . . 12 $/\$
208	207	csbeq1d 3403	. . . . . . . . . . 11 $/\$
209	109	imaeq2d 5185	. . . . . . . . . . . . . . . . 17
210	209	xpeq1d 4874	. . . . . . . . . . . . . . . 16
211	113	imaeq2d 5185	. . . . . . . . . . . . . . . . 17
212	211	xpeq1d 4874	. . . . . . . . . . . . . . . 16
213	210, 212	uneq12d 3622	. . . . . . . . . . . . . . 15
214	213	oveq2d 6319	. . . . . . . . . . . . . 14
215	214	adantl 468	. . . . . . . . . . . . 13 $/\$
216	40, 215	csbied 3423	. . . . . . . . . . . 12
217	216	adantr 467	. . . . . . . . . . 11 $/\$
218	208, 217	eqtrd 2464	. . . . . . . . . 10 $/\$
219		ovex 6331	. . . . . . . . . . 11
220	219	a1i 11	. . . . . . . . . 10
221	201, 218, 40, 220	fvmptd 5968	. . . . . . . . 9
222	221	fveq1d 5881	. . . . . . . 8
223	222	adantr 467	. . . . . . 7 $/\$
224	18	sselda 3465	. . . . . . . 8 $/\$
225		xp1st 6835	. . . . . . . . . . 11 ..^ ..^
226		elmapfn 7500	. . . . . . . . . . 11 ..^
227	8, 225, 226	3syl 18	. . . . . . . . . 10
228	227	adantr 467	. . . . . . . . 9 $/\$
229		fnconstg 5786	. . . . . . . . . . . . . 14
230	137, 229	ax-mp 5	. . . . . . . . . . . . 13
231		fnconstg 5786	. . . . . . . . . . . . . 14
232	140, 231	ax-mp 5	. . . . . . . . . . . . 13
233	230, 232	pm3.2i 457	. . . . . . . . . . . 12 $/\$
234		dff1o3 5835	. . . . . . . . . . . . . . 15 $/\$
235	234	simprbi 466	. . . . . . . . . . . . . 14
236		imain 5675	. . . . . . . . . . . . . 14
237	14, 235, 236	3syl 18	. . . . . . . . . . . . 13
238	64	imaeq2d 5185	. . . . . . . . . . . . . 14
239		ima0 5200	. . . . . . . . . . . . . 14
240	238, 239	syl6eq 2480	. . . . . . . . . . . . 13
241	237, 240	eqtr3d 2466	. . . . . . . . . . . 12
242		fnun 5698	. . . . . . . . . . . 12 $/\$ $/\$
243	233, 241, 242	sylancr 668	. . . . . . . . . . 11
244		imaundi 5265	. . . . . . . . . . . . 13
245	55	imaeq2d 5185	. . . . . . . . . . . . . 14
246		f1ofo 5836	. . . . . . . . . . . . . . 15
247		foima 5813	. . . . . . . . . . . . . . 15
248	14, 246, 247	3syl 18	. . . . . . . . . . . . . 14
249	245, 248	eqtr3d 2466	. . . . . . . . . . . . 13
250	244, 249	syl5eqr 2478	. . . . . . . . . . . 12
251	250	fneq2d 5683	. . . . . . . . . . 11
252	243, 251	mpbid 214	. . . . . . . . . 10
253	252	adantr 467	. . . . . . . . 9 $/\$