poimirlem23 - Mathbox for Brendan Leahy

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

Theorem poimirlem23 33432

Description: Lemma for poimir 33442, two ways of expressing the property that a face is not on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0
poimirlem23.1	..^
poimirlem23.2
poimirlem23.3

**Assertion**
Ref	Expression
poimirlem23	$/\$ $/\$

Distinct variable groups:

**Proof of Theorem poimirlem23**
Step	Hyp	Ref	Expression
1		ovex 6678	. . . . . 6
2	1	csbex 4793	. . . . 5
3	2	rgenw 2924	. . . 4
4		eqid 2622	. . . . 5
5		fveq1 6190	. . . . . . 7
6	5	neeq1d 2853	. . . . . 6
7		df-ne 2795	. . . . . 6
8	6, 7	syl6bb 276	. . . . 5
9	4, 8	rexrnmpt 6369	. . . 4
10	3, 9	ax-mp 5	. . 3
11		rexnal 2995	. . 3
12	10, 11	bitri 264	. 2
13		poimir.0	. . . . . . . . . . 11
14	13	nnzd 11481	. . . . . . . . . 10
15		poimirlem23.3	. . . . . . . . . . 11
16		elfzelz 12342	. . . . . . . . . . 11
17	15, 16	syl 17	. . . . . . . . . 10
18		zlem1lt 11429	. . . . . . . . . 10 $/\$
19	14, 17, 18	syl2anc 693	. . . . . . . . 9
20		elfzle2 12345	. . . . . . . . . . 11
21	15, 20	syl 17	. . . . . . . . . 10
22	17	zred 11482	. . . . . . . . . . . 12
23	13	nnred 11035	. . . . . . . . . . . 12
24	22, 23	letri3d 10179	. . . . . . . . . . 11 $/\$
25	24	biimprd 238	. . . . . . . . . 10 $/\$
26	21, 25	mpand 711	. . . . . . . . 9
27	19, 26	sylbird 250	. . . . . . . 8
28	27	necon3ad 2807	. . . . . . 7
29		nnm1nn0 11334	. . . . . . . . . . . . 13
30	13, 29	syl 17	. . . . . . . . . . . 12
31		nn0fz0 12437	. . . . . . . . . . . 12
32	30, 31	sylib 208	. . . . . . . . . . 11
33	32	adantr 481	. . . . . . . . . 10 $/\$
34		iffalse 4095	. . . . . . . . . . . . . . . 16
35	13	nncnd 11036	. . . . . . . . . . . . . . . . 17
36		npcan1 10455	. . . . . . . . . . . . . . . . 17
37	35, 36	syl 17	. . . . . . . . . . . . . . . 16
38	34, 37	sylan9eqr 2678	. . . . . . . . . . . . . . 15 $/\$
39	38	csbeq1d 3540	. . . . . . . . . . . . . 14 $/\$
40		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21
41	40	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . 20
42	41	xpeq1d 5138	. . . . . . . . . . . . . . . . . . 19
43		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
44	43	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21
45	44	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . 20
46	45	xpeq1d 5138	. . . . . . . . . . . . . . . . . . 19
47	42, 46	uneq12d 3768	. . . . . . . . . . . . . . . . . 18
48		poimirlem23.2	. . . . . . . . . . . . . . . . . . . . . 22
49		f1ofo 6144	. . . . . . . . . . . . . . . . . . . . . 22
50		foima 6120	. . . . . . . . . . . . . . . . . . . . . 22
51	48, 49, 50	3syl 18	. . . . . . . . . . . . . . . . . . . . 21
52	51	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . 20
53	23	ltp1d 10954	. . . . . . . . . . . . . . . . . . . . . . . 24
54	14	peano2zd 11485	. . . . . . . . . . . . . . . . . . . . . . . . 25
55		fzn 12357	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
56	54, 14, 55	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24
57	53, 56	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23
58	57	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . . 22
59	58	xpeq1d 5138	. . . . . . . . . . . . . . . . . . . . 21
60		ima0 5481	. . . . . . . . . . . . . . . . . . . . . . 23
61	60	xpeq1i 5135	. . . . . . . . . . . . . . . . . . . . . 22
62		0xp 5199	. . . . . . . . . . . . . . . . . . . . . 22
63	61, 62	eqtri 2644	. . . . . . . . . . . . . . . . . . . . 21
64	59, 63	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20
65	52, 64	uneq12d 3768	. . . . . . . . . . . . . . . . . . 19
66		un0 3967	. . . . . . . . . . . . . . . . . . 19
67	65, 66	syl6eq 2672	. . . . . . . . . . . . . . . . . 18
68	47, 67	sylan9eqr 2678	. . . . . . . . . . . . . . . . 17 $/\$
69	68	oveq2d 6666	. . . . . . . . . . . . . . . 16 $/\$
70	13, 69	csbied 3560	. . . . . . . . . . . . . . 15
71	70	adantr 481	. . . . . . . . . . . . . 14 $/\$
72	39, 71	eqtrd 2656	. . . . . . . . . . . . 13 $/\$
73	72	fveq1d 6193	. . . . . . . . . . . 12 $/\$
74		elfzonn0 12512	. . . . . . . . . . . . . . . . . . 19 ..^
75		nn0p1nn 11332	. . . . . . . . . . . . . . . . . . 19
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . 18 ..^
77		elsni 4194	. . . . . . . . . . . . . . . . . . . 20
78	77	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19
79	78	eleq1d 2686	. . . . . . . . . . . . . . . . . 18
80	76, 79	syl5ibrcom 237	. . . . . . . . . . . . . . . . 17 ..^
81	80	imp 445	. . . . . . . . . . . . . . . 16 ..^ $/\$
82	81	adantl 482	. . . . . . . . . . . . . . 15 $/\$ ..^ $/\$
83		poimirlem23.1	. . . . . . . . . . . . . . 15 ..^
84		1ex 10035	. . . . . . . . . . . . . . . . 17
85	84	fconst 6091	. . . . . . . . . . . . . . . 16
86	85	a1i 11	. . . . . . . . . . . . . . 15
87		ovexd 6680	. . . . . . . . . . . . . . 15
88		inidm 3822	. . . . . . . . . . . . . . 15
89	82, 83, 86, 87, 87, 88	off 6912	. . . . . . . . . . . . . 14
90		elfz1end 12371	. . . . . . . . . . . . . . 15
91	13, 90	sylib 208	. . . . . . . . . . . . . 14
92	89, 91	ffvelrnd 6360	. . . . . . . . . . . . 13
93	92	adantr 481	. . . . . . . . . . . 12 $/\$
94	73, 93	eqeltrd 2701	. . . . . . . . . . 11 $/\$
95	94	nnne0d 11065	. . . . . . . . . 10 $/\$
96		breq1 4656	. . . . . . . . . . . . . . . 16
97		id 22	. . . . . . . . . . . . . . . 16
98		oveq1 6657	. . . . . . . . . . . . . . . 16
99	96, 97, 98	ifbieq12d 4113	. . . . . . . . . . . . . . 15
100	99	csbeq1d 3540	. . . . . . . . . . . . . 14
101	100	fveq1d 6193	. . . . . . . . . . . . 13
102	101	neeq1d 2853	. . . . . . . . . . . 12
103	7, 102	syl5bbr 274	. . . . . . . . . . 11
104	103	rspcev 3309	. . . . . . . . . 10 $/\$
105	33, 95, 104	syl2anc 693	. . . . . . . . 9 $/\$
106	105, 11	sylib 208	. . . . . . . 8 $/\$
107	106	ex 450	. . . . . . 7
108	28, 107	syld 47	. . . . . 6
109	108	necon4ad 2813	. . . . 5
110	109	pm4.71rd 667	. . . 4 $/\$
111	30	nn0zd 11480	. . . . . . . . . . . . 13
112		uzid 11702	. . . . . . . . . . . . 13
113		peano2uz 11741	. . . . . . . . . . . . 13
114	111, 112, 113	3syl 18	. . . . . . . . . . . 12
115	37, 114	eqeltrrd 2702	. . . . . . . . . . 11
116		fzss2 12381	. . . . . . . . . . 11
117	115, 116	syl 17	. . . . . . . . . 10
118	117	sselda 3603	. . . . . . . . 9 $/\$
119	91	adantr 481	. . . . . . . . . . . 12 $/\$
120		ffn 6045	. . . . . . . . . . . . . . 15 ..^
121	83, 120	syl 17	. . . . . . . . . . . . . 14
122	121	adantr 481	. . . . . . . . . . . . 13 $/\$
123	84	fconst 6091	. . . . . . . . . . . . . . . . 17
124		c0ex 10034	. . . . . . . . . . . . . . . . . 18
125	124	fconst 6091	. . . . . . . . . . . . . . . . 17
126	123, 125	pm3.2i 471	. . . . . . . . . . . . . . . 16 $/\$
127		dff1o3 6143	. . . . . . . . . . . . . . . . . . 19 $/\$
128	127	simprbi 480	. . . . . . . . . . . . . . . . . 18
129		imain 5974	. . . . . . . . . . . . . . . . . 18
130	48, 128, 129	3syl 18	. . . . . . . . . . . . . . . . 17
131		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . . 22
132	131	zred 11482	. . . . . . . . . . . . . . . . . . . . 21
133	132	ltp1d 10954	. . . . . . . . . . . . . . . . . . . 20
134		fzdisj 12368	. . . . . . . . . . . . . . . . . . . 20
135	133, 134	syl 17	. . . . . . . . . . . . . . . . . . 19
136	135	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18
137	136, 60	syl6eq 2672	. . . . . . . . . . . . . . . . 17
138	130, 137	sylan9req 2677	. . . . . . . . . . . . . . . 16 $/\$
139		fun 6066	. . . . . . . . . . . . . . . 16 $/\$ $/\$
140	126, 138, 139	sylancr 695	. . . . . . . . . . . . . . 15 $/\$
141		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . . 22
142	141, 75	syl 17	. . . . . . . . . . . . . . . . . . . . 21
143		nnuz 11723	. . . . . . . . . . . . . . . . . . . . 21
144	142, 143	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . 20
145		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . 20
146		fzsplit2 12366	. . . . . . . . . . . . . . . . . . . 20 $/\$
147	144, 145, 146	syl2anc 693	. . . . . . . . . . . . . . . . . . 19
148	147	imaeq2d 5466	. . . . . . . . . . . . . . . . . 18
149		imaundi 5545	. . . . . . . . . . . . . . . . . 18
150	148, 149	syl6req 2673	. . . . . . . . . . . . . . . . 17
151	150, 51	sylan9eqr 2678	. . . . . . . . . . . . . . . 16 $/\$
152	151	feq2d 6031	. . . . . . . . . . . . . . 15 $/\$
153	140, 152	mpbid 222	. . . . . . . . . . . . . 14 $/\$
154		ffn 6045	. . . . . . . . . . . . . 14
155	153, 154	syl 17	. . . . . . . . . . . . 13 $/\$
156		ovexd 6680	. . . . . . . . . . . . 13 $/\$
157		eqidd 2623	. . . . . . . . . . . . 13 $/\$ $/\$
158		eqidd 2623	. . . . . . . . . . . . 13 $/\$ $/\$
159	122, 155, 156, 156, 88, 157, 158	ofval 6906	. . . . . . . . . . . 12 $/\$ $/\$
160	119, 159	mpdan 702	. . . . . . . . . . 11 $/\$
161	160	eqeq1d 2624	. . . . . . . . . 10 $/\$
162	83, 91	ffvelrnd 6360	. . . . . . . . . . . . . 14 ..^
163		elfzonn0 12512	. . . . . . . . . . . . . 14 ..^
164	162, 163	syl 17	. . . . . . . . . . . . 13
165	164	nn0red 11352	. . . . . . . . . . . 12
166	165	adantr 481	. . . . . . . . . . 11 $/\$
167	164	nn0ge0d 11354	. . . . . . . . . . . 12
168	167	adantr 481	. . . . . . . . . . 11 $/\$
169		1re 10039	. . . . . . . . . . . . . 14
170		snssi 4339	. . . . . . . . . . . . . 14
171	169, 170	ax-mp 5	. . . . . . . . . . . . 13
172		0re 10040	. . . . . . . . . . . . . 14
173		snssi 4339	. . . . . . . . . . . . . 14
174	172, 173	ax-mp 5	. . . . . . . . . . . . 13
175	171, 174	unssi 3788	. . . . . . . . . . . 12
176	153, 119	ffvelrnd 6360	. . . . . . . . . . . 12 $/\$
177	175, 176	sseldi 3601	. . . . . . . . . . 11 $/\$
178		elun 3753	. . . . . . . . . . . . 13 $\/$
179		0le1 10551	. . . . . . . . . . . . . . 15
180		elsni 4194	. . . . . . . . . . . . . . 15
181	179, 180	syl5breqr 4691	. . . . . . . . . . . . . 14
182		0le0 11110	. . . . . . . . . . . . . . 15
183		elsni 4194	. . . . . . . . . . . . . . 15
184	182, 183	syl5breqr 4691	. . . . . . . . . . . . . 14
185	181, 184	jaoi 394	. . . . . . . . . . . . 13 $\/$
186	178, 185	sylbi 207	. . . . . . . . . . . 12
187	176, 186	syl 17	. . . . . . . . . . 11 $/\$
188		add20 10540	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
189	166, 168, 177, 187, 188	syl22anc 1327	. . . . . . . . . 10 $/\$ $/\$
190	161, 189	bitrd 268	. . . . . . . . 9 $/\$ $/\$
191	118, 190	syldan 487	. . . . . . . 8 $/\$ $/\$
192	191	ralbidva 2985	. . . . . . 7 $/\$
193	192	adantr 481	. . . . . 6 $/\$ $/\$
194		breq2 4657	. . . . . . . . . . . . . 14
195	194	ifbid 4108	. . . . . . . . . . . . 13
196		elfzelz 12342	. . . . . . . . . . . . . . . . 17
197	196	zred 11482	. . . . . . . . . . . . . . . 16
198	197	adantl 482	. . . . . . . . . . . . . . 15 $/\$
199	30	nn0red 11352	. . . . . . . . . . . . . . . 16
200	199	adantr 481	. . . . . . . . . . . . . . 15 $/\$
201	23	adantr 481	. . . . . . . . . . . . . . 15 $/\$
202		elfzle2 12345	. . . . . . . . . . . . . . . 16
203	202	adantl 482	. . . . . . . . . . . . . . 15 $/\$
204	23	ltm1d 10956	. . . . . . . . . . . . . . . 16
205	204	adantr 481	. . . . . . . . . . . . . . 15 $/\$
206	198, 200, 201, 203, 205	lelttrd 10195	. . . . . . . . . . . . . 14 $/\$
207	206	iftrued 4094	. . . . . . . . . . . . 13 $/\$
208	195, 207	sylan9eqr 2678	. . . . . . . . . . . 12 $/\$ $/\$
209	208	an32s 846	. . . . . . . . . . 11 $/\$ $/\$
210	209	csbeq1d 3540	. . . . . . . . . 10 $/\$ $/\$
211	210	fveq1d 6193	. . . . . . . . 9 $/\$ $/\$
212	211	eqeq1d 2624	. . . . . . . 8 $/\$ $/\$
213	212	ralbidva 2985	. . . . . . 7 $/\$
214		nfv 1843	. . . . . . . 8
215		nfcsb1v 3549	. . . . . . . . . 10
216		nfcv 2764	. . . . . . . . . 10
217	215, 216	nffv 6198	. . . . . . . . 9
218	217	nfeq1 2778	. . . . . . . 8
219		csbeq1a 3542	. . . . . . . . . 10
220	219	fveq1d 6193	. . . . . . . . 9
221	220	eqeq1d 2624	. . . . . . . 8
222	214, 218, 221	cbvral 3167	. . . . . . 7
223	213, 222	syl6bbr 278	. . . . . 6 $/\$
224		ne0i 3921	. . . . . . . . . 10
225		r19.3rzv 4064	. . . . . . . . . 10
226	32, 224, 225	3syl 18	. . . . . . . . 9
227		elfzelz 12342	. . . . . . . . . . . . . . . . . . . . 21
228	227	zred 11482	. . . . . . . . . . . . . . . . . . . 20
229	228	ltp1d 10954	. . . . . . . . . . . . . . . . . . 19
230	229, 134	syl 17	. . . . . . . . . . . . . . . . . 18
231	230	imaeq2d 5466	. . . . . . . . . . . . . . . . 17
232	231, 60	syl6eq 2672	. . . . . . . . . . . . . . . 16
233	130, 232	sylan9req 2677	. . . . . . . . . . . . . . 15 $/\$
234	233	adantlr 751	. . . . . . . . . . . . . 14 $/\$ $/\$
235		simplr 792	. . . . . . . . . . . . . . 15 $/\$ $/\$
236		f1ofn 6138	. . . . . . . . . . . . . . . . . . 19
237	48, 236	syl 17	. . . . . . . . . . . . . . . . . 18
238	237	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
239		elfznn0 12433	. . . . . . . . . . . . . . . . . . . . 21
240	239, 75	syl 17	. . . . . . . . . . . . . . . . . . . 20
241	240, 143	syl6eleq 2711	. . . . . . . . . . . . . . . . . . 19
242		fzss1 12380	. . . . . . . . . . . . . . . . . . 19
243	241, 242	syl 17	. . . . . . . . . . . . . . . . . 18
244	243	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
245	37	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
246		elfzuz3 12339	. . . . . . . . . . . . . . . . . . . . 21
247		eluzp1p1 11713	. . . . . . . . . . . . . . . . . . . . 21
248	246, 247	syl 17	. . . . . . . . . . . . . . . . . . . 20
249	248	adantl 482	. . . . . . . . . . . . . . . . . . 19 $/\$
250	245, 249	eqeltrrd 2702	. . . . . . . . . . . . . . . . . 18 $/\$
251		eluzfz2 12349	. . . . . . . . . . . . . . . . . 18
252	250, 251	syl 17	. . . . . . . . . . . . . . . . 17 $/\$
253		fnfvima 6496	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
254	238, 244, 252, 253	syl3anc 1326	. . . . . . . . . . . . . . . 16 $/\$
255	254	adantlr 751	. . . . . . . . . . . . . . 15 $/\$ $/\$
256	235, 255	eqeltrrd 2702	. . . . . . . . . . . . . 14 $/\$ $/\$
257		fnconstg 6093	. . . . . . . . . . . . . . . 16
258	84, 257	ax-mp 5	. . . . . . . . . . . . . . 15
259		fnconstg 6093	. . . . . . . . . . . . . . . 16
260	124, 259	ax-mp 5	. . . . . . . . . . . . . . 15
261		fvun2 6270	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
262	258, 260, 261	mp3an12 1414	. . . . . . . . . . . . . 14 $/\$
263	234, 256, 262	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$
264	124	fvconst2 6469	. . . . . . . . . . . . . 14
265	256, 264	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
266	263, 265	eqtrd 2656	. . . . . . . . . . . 12 $/\$ $/\$
267	266	ralrimiva 2966	. . . . . . . . . . 11 $/\$
268	267	ex 450	. . . . . . . . . 10
269	32	adantr 481	. . . . . . . . . . . . . 14 $/\$
270		ax-1ne0 10005	. . . . . . . . . . . . . . 15
271		imain 5974	. . . . . . . . . . . . . . . . . . . . 21
272	48, 128, 271	3syl 18	. . . . . . . . . . . . . . . . . . . 20
273	204, 37	breqtrrd 4681	. . . . . . . . . . . . . . . . . . . . . . 23
274		fzdisj 12368	. . . . . . . . . . . . . . . . . . . . . . 23
275	273, 274	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
276	275	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . 21
277	276, 60	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20
278	272, 277	eqtr3d 2658	. . . . . . . . . . . . . . . . . . 19
279	278	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
280	91	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
281		elimasni 5492	. . . . . . . . . . . . . . . . . . . . . . 23
282		fnbrfvb 6236	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
283	237, 91, 282	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23
284	281, 283	syl5ibr 236	. . . . . . . . . . . . . . . . . . . . . 22
285	284	necon3ad 2807	. . . . . . . . . . . . . . . . . . . . 21
286	285	imp 445	. . . . . . . . . . . . . . . . . . . 20 $/\$
287	280, 286	eldifd 3585	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
288		imadif 5973	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$
289	48, 128, 288	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
290		difun2 4048	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
291	13, 143	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
292		fzm1 12420	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\/$
293	291, 292	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\/$
294		elun 3753	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\/$
295		velsn 4193	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
296	295	orbi2i 541	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\/$ $\/$
297	294, 296	bitri 264	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\/$
298	293, 297	syl6rbbr 279	. . . . . . . . . . . . . . . . . . . . . . . . 25
299	298	eqrdv 2620	. . . . . . . . . . . . . . . . . . . . . . . 24
300	299	difeq1d 3727	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
301	199, 23	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . . . 26
302	204, 301	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . 25
303		elfzle2 12345	. . . . . . . . . . . . . . . . . . . . . . . . 25
304	302, 303	nsyl 135	. . . . . . . . . . . . . . . . . . . . . . . 24
305		difsn 4328	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
306	304, 305	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $\$
307	290, 300, 306	3eqtr3a 2680	. . . . . . . . . . . . . . . . . . . . . 22 $\$
308	307	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . . 21 $\$
309	51	difeq1d 3727	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
310	289, 308, 309	3eqtr3rd 2665	. . . . . . . . . . . . . . . . . . . 20 $\$
311	310	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
312	287, 311	eleqtrd 2703	. . . . . . . . . . . . . . . . . 18 $/\$
313		fnconstg 6093	. . . . . . . . . . . . . . . . . . . 20
314	84, 313	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
315		fnconstg 6093	. . . . . . . . . . . . . . . . . . . 20
316	124, 315	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
317		fvun1 6269	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
318	314, 316, 317	mp3an12 1414	. . . . . . . . . . . . . . . . . 18 $/\$
319	279, 312, 318	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$
320	84	fvconst2 6469	. . . . . . . . . . . . . . . . . 18
321	312, 320	syl 17	. . . . . . . . . . . . . . . . 17 $/\$
322	319, 321	eqtrd 2656	. . . . . . . . . . . . . . . 16 $/\$
323	322	neeq1d 2853	. . . . . . . . . . . . . . 15 $/\$
324	270, 323	mpbiri 248	. . . . . . . . . . . . . 14 $/\$
325		df-ne 2795	. . . . . . . . . . . . . . . 16
326		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21
327	326	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . 20
328	327	xpeq1d 5138	. . . . . . . . . . . . . . . . . . 19
329		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22
330	329	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21
331	330	imaeq2d 5466	. . . . . . . . . . . . . . . . . . . 20
332	331	xpeq1d 5138	. . . . . . . . . . . . . . . . . . 19
333	328, 332	uneq12d 3768	. . . . . . . . . . . . . . . . . 18
334	333	fveq1d 6193	. . . . . . . . . . . . . . . . 17
335	334	neeq1d 2853	. . . . . . . . . . . . . . . 16
336	325, 335	syl5bbr 274	. . . . . . . . . . . . . . 15
337	336	rspcev 3309	. . . . . . . . . . . . . 14 $/\$
338	269, 324, 337	syl2anc 693	. . . . . . . . . . . . 13 $/\$
339	338	ex 450	. . . . . . . . . . . 12
340		rexnal 2995	. . . . . . . . . . . 12
341	339, 340	syl6ib 241	. . . . . . . . . . 11
342	341	necon4ad 2813	. . . . . . . . . 10
343	268, 342	impbid 202	. . . . . . . . 9
344	226, 343	anbi12d 747	. . . . . . . 8 $/\$ $/\$
345		r19.26 3064	. . . . . . . 8 $/\$ $/\$
346	344, 345	syl6bbr 278	. . . . . . 7 $/\$ $/\$
347	346	adantr 481	. . . . . 6 $/\$ $/\$ $/\$
348	193, 223, 347	3bitr4d 300	. . . . 5 $/\$ $/\$
349	348	pm5.32da 673	. . . 4 $/\$ $/\$ $/\$
350	110, 349	bitrd 268	. . 3 $/\$ $/\$
351	350	notbid 308	. 2 $/\$ $/\$
352	12, 351	syl5bb 272	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

cvv 3200

csb 3533 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cif 4086

csn 4177 class class class wbr 4653

cmpt 4729

cxp 5112

ccnv 5113

crn 5115

cima 5117

wfun 5882

wfn 5883

wf 5884

wfo 5886

wf1o 5887

cfv 5888 (class class class)co 6650

cof 6895

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-fal 1489 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-of 6897 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 df-fzo 12466

This theorem is referenced by: poimirlem24 33433

W3C validator