ackbij1lem16 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ackbij1lem16		Unicode version

Theorem ackbij1lem16 8079

Description: Lemma for ackbij1 8082. (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 3529	. . . . . . . . 9
2	1	sseli 3312	. . . . . . . 8
3	2	elpwid 3776	. . . . . . 7
4	3	adantr 452	. . . . . 6 $/\$
5	1	sseli 3312	. . . . . . . 8
6	5	elpwid 3776	. . . . . . 7
7	6	adantl 453	. . . . . 6 $/\$
8	4, 7	unssd 3491	. . . . 5 $/\$
9		inss2 3530	. . . . . . 7
10	9	sseli 3312	. . . . . 6
11	9	sseli 3312	. . . . . 6
12		unfi 7341	. . . . . 6 $/\$
13	10, 11, 12	syl2an 464	. . . . 5 $/\$
14		nnunifi 7325	. . . . 5 $/\$
15	8, 13, 14	syl2anc 643	. . . 4 $/\$
16		peano2 4832	. . . 4
17	15, 16	syl 16	. . 3 $/\$
18		ineq2 3504	. . . . . . . 8
19	18	fveq2d 5699	. . . . . . 7
20		ineq2 3504	. . . . . . . 8
21	20	fveq2d 5699	. . . . . . 7
22	19, 21	eqeq12d 2426	. . . . . 6
23	18, 20	eqeq12d 2426	. . . . . 6
24	22, 23	imbi12d 312	. . . . 5
25	24	imbi2d 308	. . . 4 $/\$ $/\$
26		ineq2 3504	. . . . . . . 8
27	26	fveq2d 5699	. . . . . . 7
28		ineq2 3504	. . . . . . . 8
29	28	fveq2d 5699	. . . . . . 7
30	27, 29	eqeq12d 2426	. . . . . 6
31	26, 28	eqeq12d 2426	. . . . . 6
32	30, 31	imbi12d 312	. . . . 5
33	32	imbi2d 308	. . . 4 $/\$ $/\$
34		ineq2 3504	. . . . . . . 8
35	34	fveq2d 5699	. . . . . . 7
36		ineq2 3504	. . . . . . . 8
37	36	fveq2d 5699	. . . . . . 7
38	35, 37	eqeq12d 2426	. . . . . 6
39	34, 36	eqeq12d 2426	. . . . . 6
40	38, 39	imbi12d 312	. . . . 5
41	40	imbi2d 308	. . . 4 $/\$ $/\$
42		ineq2 3504	. . . . . . . 8
43	42	fveq2d 5699	. . . . . . 7
44		ineq2 3504	. . . . . . . 8
45	44	fveq2d 5699	. . . . . . 7
46	43, 45	eqeq12d 2426	. . . . . 6
47	42, 44	eqeq12d 2426	. . . . . 6
48	46, 47	imbi12d 312	. . . . 5
49	48	imbi2d 308	. . . 4 $/\$ $/\$
50		in0 3621	. . . . . 6
51		in0 3621	. . . . . 6
52	50, 51	eqtr4i 2435	. . . . 5
53	52	a1ii 25	. . . 4 $/\$
54		simp13 989	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
55		3simpa 954	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
56		ackbij1lem2 8065	. . . . . . . . . . . . . . . . 17
57	56	fveq2d 5699	. . . . . . . . . . . . . . . 16
58	57	3ad2ant2 979	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
59		ackbij1lem4 8067	. . . . . . . . . . . . . . . . . 18
60	59	adantr 452	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
61		simprl 733	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
62		inss1 3529	. . . . . . . . . . . . . . . . . 18
63		ackbij.f	. . . . . . . . . . . . . . . . . . 19
64	63	ackbij1lem11 8074	. . . . . . . . . . . . . . . . . 18 $/\$
65	61, 62, 64	sylancl 644	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
66		incom 3501	. . . . . . . . . . . . . . . . . 18
67		inss2 3530	. . . . . . . . . . . . . . . . . . 19
68		nnord 4820	. . . . . . . . . . . . . . . . . . . . 21
69		orddisj 4587	. . . . . . . . . . . . . . . . . . . . 21
70	68, 69	syl 16	. . . . . . . . . . . . . . . . . . . 20
71	70	adantr 452	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
72		ssdisj 3645	. . . . . . . . . . . . . . . . . . 19 $/\$
73	67, 71, 72	sylancr 645	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
74	66, 73	syl5eq 2456	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
75	63	ackbij1lem9 8072	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
76	60, 65, 74, 75	syl3anc 1184	. . . . . . . . . . . . . . . 16 $/\$ $/\$
77	76	3ad2ant1 978	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
78	58, 77	eqtrd 2444	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
79	55, 78	syl3an1 1217	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
80		ackbij1lem2 8065	. . . . . . . . . . . . . . . . 17
81	80	fveq2d 5699	. . . . . . . . . . . . . . . 16
82	81	3ad2ant3 980	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
83		simprr 734	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
84		inss1 3529	. . . . . . . . . . . . . . . . . 18
85	63	ackbij1lem11 8074	. . . . . . . . . . . . . . . . . 18 $/\$
86	83, 84, 85	sylancl 644	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
87		incom 3501	. . . . . . . . . . . . . . . . . 18
88		inss2 3530	. . . . . . . . . . . . . . . . . . 19
89		ssdisj 3645	. . . . . . . . . . . . . . . . . . 19 $/\$
90	88, 71, 89	sylancr 645	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
91	87, 90	syl5eq 2456	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
92	63	ackbij1lem9 8072	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
93	60, 86, 91, 92	syl3anc 1184	. . . . . . . . . . . . . . . 16 $/\$ $/\$
94	93	3ad2ant1 978	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
95	82, 94	eqtrd 2444	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
96	55, 95	syl3an1 1217	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
97	54, 79, 96	3eqtr3d 2452	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
98	63	ackbij1lem10 8073	. . . . . . . . . . . . . . . . 17
99	98	ffvelrni 5836	. . . . . . . . . . . . . . . 16
100	60, 99	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
101	98	ffvelrni 5836	. . . . . . . . . . . . . . . 16
102	65, 101	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
103	98	ffvelrni 5836	. . . . . . . . . . . . . . . 16
104	86, 103	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$
105		nnacan 6838	. . . . . . . . . . . . . . 15 $/\$ $/\$
106	100, 102, 104, 105	syl3anc 1184	. . . . . . . . . . . . . 14 $/\$ $/\$
107	106	3adant3 977	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
108	107	3ad2ant1 978	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
109	97, 108	mpbid 202	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
110		uneq2 3463	. . . . . . . . . . . . . . 15
111	110	adantl 453	. . . . . . . . . . . . . 14 $/\$ $/\$
112	56	ad2antrr 707	. . . . . . . . . . . . . 14 $/\$ $/\$
113	80	ad2antlr 708	. . . . . . . . . . . . . 14 $/\$ $/\$
114	111, 112, 113	3eqtr4d 2454	. . . . . . . . . . . . 13 $/\$ $/\$
115	114	ex 424	. . . . . . . . . . . 12 $/\$
116	115	3adant1 975	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
117	109, 116	embantd 52	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
118	117	3exp 1152	. . . . . . . . 9 $/\$ $/\$ $/\$
119		simp13 989	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
120	119	eqcomd 2417	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
121		simp12r 1071	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
122		simp12l 1070	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
123		simp11 987	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
124		simp3 959	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
125		simp2 958	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
126	63	ackbij1lem15 8078	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
127	121, 122, 123, 124, 125, 126	syl23anc 1191	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
128	120, 127	pm2.21dd 101	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
129	128	3exp 1152	. . . . . . . . 9 $/\$ $/\$ $/\$
130	118, 129	pm2.61d 152	. . . . . . . 8 $/\$ $/\$ $/\$
131		simp13 989	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
132		simp12l 1070	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
133		simp12r 1071	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
134		simp11 987	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
135		simp2 958	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
136		simp3 959	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
137	63	ackbij1lem15 8078	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
138	132, 133, 134, 135, 136, 137	syl23anc 1191	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
139	131, 138	pm2.21dd 101	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
140	139	3exp 1152	. . . . . . . . 9 $/\$ $/\$ $/\$
141		simp13 989	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
142		ackbij1lem1 8064	. . . . . . . . . . . . . . . . 17
143	142	adantr 452	. . . . . . . . . . . . . . . 16 $/\$
144	143	fveq2d 5699	. . . . . . . . . . . . . . 15 $/\$
145		ackbij1lem1 8064	. . . . . . . . . . . . . . . . 17
146	145	adantl 453	. . . . . . . . . . . . . . . 16 $/\$
147	146	fveq2d 5699	. . . . . . . . . . . . . . 15 $/\$
148	144, 147	eqeq12d 2426	. . . . . . . . . . . . . 14 $/\$
149	148	biimpd 199	. . . . . . . . . . . . 13 $/\$
150	149	3adant1 975	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
151	141, 150	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
152	143, 146	eqeq12d 2426	. . . . . . . . . . . . 13 $/\$
153	152	biimprd 215	. . . . . . . . . . . 12 $/\$
154	153	3adant1 975	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
155	151, 154	embantd 52	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
156	155	3exp 1152	. . . . . . . . 9 $/\$ $/\$ $/\$
157	140, 156	pm2.61d 152	. . . . . . . 8 $/\$ $/\$ $/\$
158	130, 157	pm2.61d 152	. . . . . . 7 $/\$ $/\$ $/\$
159	158	3exp 1152	. . . . . 6 $/\$
160	159	com34 79	. . . . 5 $/\$
161	160	a2d 24	. . . 4 $/\$ $/\$
162	25, 33, 41, 49, 53, 161	finds 4838	. . 3 $/\$
163	17, 162	mpcom 34	. 2 $/\$
164		omsson 4816	. . . . . . . 8
165	8, 164	syl6ss 3328	. . . . . . 7 $/\$
166		onsucuni 4775	. . . . . . 7
167	165, 166	syl 16	. . . . . 6 $/\$
168	167	unssad 3492	. . . . 5 $/\$
169		df-ss 3302	. . . . 5
170	168, 169	sylib 189	. . . 4 $/\$
171	170	fveq2d 5699	. . 3 $/\$
172	167	unssbd 3493	. . . . 5 $/\$
173		df-ss 3302	. . . . 5
174	172, 173	sylib 189	. . . 4 $/\$
175	174	fveq2d 5699	. . 3 $/\$
176	171, 175	eqeq12d 2426	. 2 $/\$
177	170, 174	eqeq12d 2426	. 2 $/\$
178	163, 176, 177	3imtr3d 259	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

cun 3286

cin 3287

wss 3288

c0 3596

cpw 3767

csn 3782

cuni 3983

ciun 4061

cmpt 4234

word 4548

con0 4549

csuc 4551

com 4812

cxp 4843

cfv 5421 (class class class)co 6048

coa 6688

cfn 7076

ccrd 7786

This theorem is referenced by: ackbij1lem17 8080

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2393 ax-rep 4288 ax-sep 4298 ax-nul 4306 ax-pow 4345 ax-pr 4371 ax-un 4668

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2266 df-mo 2267 df-clab 2399 df-cleq 2405 df-clel 2408 df-nfc 2537 df-ne 2577 df-ral 2679 df-rex 2680 df-reu 2681 df-rmo 2682 df-rab 2683 df-v 2926 df-sbc 3130 df-csb 3220 df-dif 3291 df-un 3293 df-in 3295 df-ss 3302 df-pss 3304 df-nul 3597 df-if 3708 df-pw 3769 df-sn 3788 df-pr 3789 df-tp 3790 df-op 3791 df-uni 3984 df-int 4019 df-iun 4063 df-br 4181 df-opab 4235 df-mpt 4236 df-tr 4271 df-eprel 4462 df-id 4466 df-po 4471 df-so 4472 df-fr 4509 df-we 4511 df-ord 4552 df-on 4553 df-lim 4554 df-suc 4555 df-om 4813 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5385 df-fun 5423 df-fn 5424 df-f 5425 df-f1 5426 df-fo 5427 df-f1o 5428 df-fv 5429 df-ov 6051 df-oprab 6052 df-mpt2 6053 df-1st 6316 df-2nd 6317 df-recs 6600 df-rdg 6635 df-1o 6691 df-2o 6692 df-oadd 6695 df-er 6872 df-map 6987 df-en 7077 df-dom 7078 df-sdom 7079 df-fin 7080 df-card 7790 df-cda 8012

W3C validator