Theorem ackbij1lem16 8636

Description: Lemma for ackbij1 8639. (Contributed by Stefan O'Rear, 18-Nov-2014.)

Hypothesis

Ref	Expression
ackbij.f

Assertion

Ref	Expression
ackbij1lem16

Distinct variable groups:   ,,   ,,   ,,

Proof of Theorem ackbij1lem16

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss1 3717	. . . . . . . . 9
2	1	sseli 3499	. . . . . . . 8
3	2	elpwid 4022	. . . . . . 7
4	3	adantr 465	. . . . . 6
5	1	sseli 3499	. . . . . . . 8
6	5	elpwid 4022	. . . . . . 7
7	6	adantl 466	. . . . . 6
8	4, 7	unssd 3679	. . . . 5
9		inss2 3718	. . . . . . 7
10	9	sseli 3499	. . . . . 6
11	9	sseli 3499	. . . . . 6
12		unfi 7807	. . . . . 6
13	10, 11, 12	syl2an 477	. . . . 5
14		nnunifi 7791	. . . . 5
15	8, 13, 14	syl2anc 661	. . . 4
16		peano2 6720	. . . 4
17	15, 16	syl 16	. . 3
18		ineq2 3693	. . . . . . . 8
19	18	fveq2d 5875	. . . . . . 7
20		ineq2 3693	. . . . . . . 8
21	20	fveq2d 5875	. . . . . . 7
22	19, 21	eqeq12d 2479	. . . . . 6
23	18, 20	eqeq12d 2479	. . . . . 6
24	22, 23	imbi12d 320	. . . . 5
25	24	imbi2d 316	. . . 4
26		ineq2 3693	. . . . . . . 8
27	26	fveq2d 5875	. . . . . . 7
28		ineq2 3693	. . . . . . . 8
29	28	fveq2d 5875	. . . . . . 7
30	27, 29	eqeq12d 2479	. . . . . 6
31	26, 28	eqeq12d 2479	. . . . . 6
32	30, 31	imbi12d 320	. . . . 5
33	32	imbi2d 316	. . . 4
34		ineq2 3693	. . . . . . . 8
35	34	fveq2d 5875	. . . . . . 7
36		ineq2 3693	. . . . . . . 8
37	36	fveq2d 5875	. . . . . . 7
38	35, 37	eqeq12d 2479	. . . . . 6
39	34, 36	eqeq12d 2479	. . . . . 6
40	38, 39	imbi12d 320	. . . . 5
41	40	imbi2d 316	. . . 4
42		ineq2 3693	. . . . . . . 8
43	42	fveq2d 5875	. . . . . . 7
44		ineq2 3693	. . . . . . . 8
45	44	fveq2d 5875	. . . . . . 7
46	43, 45	eqeq12d 2479	. . . . . 6
47	42, 44	eqeq12d 2479	. . . . . 6
48	46, 47	imbi12d 320	. . . . 5
49	48	imbi2d 316	. . . 4
50		in0 3811	. . . . . 6
51		in0 3811	. . . . . 6
52	50, 51	eqtr4i 2489	. . . . 5
53	52	a1ii 27	. . . 4
54		simp13 1028	. . . . . . . . . . . . 13
55		3simpa 993	. . . . . . . . . . . . . 14
56		ackbij1lem2 8622	. . . . . . . . . . . . . . . . 17
57	56	fveq2d 5875	. . . . . . . . . . . . . . . 16
58	57	3ad2ant2 1018	. . . . . . . . . . . . . . 15
59		ackbij1lem4 8624	. . . . . . . . . . . . . . . . . 18
60	59	adantr 465	. . . . . . . . . . . . . . . . 17
61		simprl 756	. . . . . . . . . . . . . . . . . 18
62		inss1 3717	. . . . . . . . . . . . . . . . . 18
63		ackbij.f	. . . . . . . . . . . . . . . . . . 19
64	63	ackbij1lem11 8631	. . . . . . . . . . . . . . . . . 18
65	61, 62, 64	sylancl 662	. . . . . . . . . . . . . . . . 17
66		incom 3690	. . . . . . . . . . . . . . . . . 18
67		inss2 3718	. . . . . . . . . . . . . . . . . . 19
68		nnord 6708	. . . . . . . . . . . . . . . . . . . . 21
69		orddisj 4921	. . . . . . . . . . . . . . . . . . . . 21
70	68, 69	syl 16	. . . . . . . . . . . . . . . . . . . 20
71	70	adantr 465	. . . . . . . . . . . . . . . . . . 19
72		ssdisj 3876	. . . . . . . . . . . . . . . . . . 19
73	67, 71, 72	sylancr 663	. . . . . . . . . . . . . . . . . 18
74	66, 73	syl5eq 2510	. . . . . . . . . . . . . . . . 17
75	63	ackbij1lem9 8629	. . . . . . . . . . . . . . . . 17
76	60, 65, 74, 75	syl3anc 1228	. . . . . . . . . . . . . . . 16
77	76	3ad2ant1 1017	. . . . . . . . . . . . . . 15
78	58, 77	eqtrd 2498	. . . . . . . . . . . . . 14
79	55, 78	syl3an1 1261	. . . . . . . . . . . . 13
80		ackbij1lem2 8622	. . . . . . . . . . . . . . . . 17
81	80	fveq2d 5875	. . . . . . . . . . . . . . . 16
82	81	3ad2ant3 1019	. . . . . . . . . . . . . . 15
83		simprr 757	. . . . . . . . . . . . . . . . . 18
84		inss1 3717	. . . . . . . . . . . . . . . . . 18
85	63	ackbij1lem11 8631	. . . . . . . . . . . . . . . . . 18
86	83, 84, 85	sylancl 662	. . . . . . . . . . . . . . . . 17
87		incom 3690	. . . . . . . . . . . . . . . . . 18
88		inss2 3718	. . . . . . . . . . . . . . . . . . 19
89		ssdisj 3876	. . . . . . . . . . . . . . . . . . 19
90	88, 71, 89	sylancr 663	. . . . . . . . . . . . . . . . . 18
91	87, 90	syl5eq 2510	. . . . . . . . . . . . . . . . 17
92	63	ackbij1lem9 8629	. . . . . . . . . . . . . . . . 17
93	60, 86, 91, 92	syl3anc 1228	. . . . . . . . . . . . . . . 16
94	93	3ad2ant1 1017	. . . . . . . . . . . . . . 15
95	82, 94	eqtrd 2498	. . . . . . . . . . . . . 14
96	55, 95	syl3an1 1261	. . . . . . . . . . . . 13
97	54, 79, 96	3eqtr3d 2506	. . . . . . . . . . . 12
98	63	ackbij1lem10 8630	. . . . . . . . . . . . . . . . 17
99	98	ffvelrni 6030	. . . . . . . . . . . . . . . 16
100	60, 99	syl 16	. . . . . . . . . . . . . . 15
101	98	ffvelrni 6030	. . . . . . . . . . . . . . . 16
102	65, 101	syl 16	. . . . . . . . . . . . . . 15
103	98	ffvelrni 6030	. . . . . . . . . . . . . . . 16
104	86, 103	syl 16	. . . . . . . . . . . . . . 15
105		nnacan 7296	. . . . . . . . . . . . . . 15
106	100, 102, 104, 105	syl3anc 1228	. . . . . . . . . . . . . 14
107	106	3adant3 1016	. . . . . . . . . . . . 13
108	107	3ad2ant1 1017	. . . . . . . . . . . 12
109	97, 108	mpbid 210	. . . . . . . . . . 11
110		uneq2 3651	. . . . . . . . . . . . . . 15
111	110	adantl 466	. . . . . . . . . . . . . 14
112	56	ad2antrr 725	. . . . . . . . . . . . . 14
113	80	ad2antlr 726	. . . . . . . . . . . . . 14
114	111, 112, 113	3eqtr4d 2508	. . . . . . . . . . . . 13
115	114	ex 434	. . . . . . . . . . . 12
116	115	3adant1 1014	. . . . . . . . . . 11
117	109, 116	embantd 54	. . . . . . . . . 10
118	117	3exp 1195	. . . . . . . . 9
119		simp13 1028	. . . . . . . . . . . 12
120	119	eqcomd 2465	. . . . . . . . . . 11
121		simp12r 1110	. . . . . . . . . . . 12
122		simp12l 1109	. . . . . . . . . . . 12
123		simp11 1026	. . . . . . . . . . . 12
124		simp3 998	. . . . . . . . . . . 12
125		simp2 997	. . . . . . . . . . . 12
126	63	ackbij1lem15 8635	. . . . . . . . . . . 12
127	121, 122, 123, 124, 125, 126	syl23anc 1235	. . . . . . . . . . 11
128	120, 127	pm2.21dd 174	. . . . . . . . . 10
129	128	3exp 1195	. . . . . . . . 9
130	118, 129	pm2.61d 158	. . . . . . . 8
131		simp13 1028	. . . . . . . . . . 11
132		simp12l 1109	. . . . . . . . . . . 12
133		simp12r 1110	. . . . . . . . . . . 12
134		simp11 1026	. . . . . . . . . . . 12
135		simp2 997	. . . . . . . . . . . 12
136		simp3 998	. . . . . . . . . . . 12
137	63	ackbij1lem15 8635	. . . . . . . . . . . 12
138	132, 133, 134, 135, 136, 137	syl23anc 1235	. . . . . . . . . . 11
139	131, 138	pm2.21dd 174	. . . . . . . . . 10
140	139	3exp 1195	. . . . . . . . 9
141		simp13 1028	. . . . . . . . . . . 12
142		ackbij1lem1 8621	. . . . . . . . . . . . . . . . 17
143	142	adantr 465	. . . . . . . . . . . . . . . 16