Theorem ackbij2lem2 8641

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

Hypotheses

Ref	Expression
ackbij.f
ackbij.g

Assertion

Ref	Expression
ackbij2lem2

Distinct variable groups:   ,,   ,,   ,,

Proof of Theorem ackbij2lem2

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

Step	Hyp	Ref	Expression
1		fveq2 5871	. . 3
2		fveq2 5871	. . 3
3	2	fveq2d 5875	. . 3
4	1, 2, 3	f1oeq123d 5818	. 2
5		fveq2 5871	. . 3
6		fveq2 5871	. . 3
7	6	fveq2d 5875	. . 3
8	5, 6, 7	f1oeq123d 5818	. 2
9		fveq2 5871	. . 3
10		fveq2 5871	. . 3
11	10	fveq2d 5875	. . 3
12	9, 10, 11	f1oeq123d 5818	. 2
13		fveq2 5871	. . 3
14		fveq2 5871	. . 3
15	14	fveq2d 5875	. . 3
16	13, 14, 15	f1oeq123d 5818	. 2
17		f1o0 5855	. . 3
18		0ex 4582	. . . . . 6
19	18	rdg0 7106	. . . . 5
20		f1oeq1 5812	. . . . 5
21	19, 20	ax-mp 5	. . . 4
22		r10 8207	. . . . 5
23	22	fveq2i 5874	. . . . . 6
24		card0 8360	. . . . . 6
25	23, 24	eqtri 2486	. . . . 5
26		f1oeq23 5815	. . . . 5
27	22, 25, 26	mp2an 672	. . . 4
28	21, 27	bitri 249	. . 3
29	17, 28	mpbir 209	. 2
30		ackbij.f	. . . . . . . . . 10
31	30	ackbij1lem17 8637	. . . . . . . . 9
32	31	a1i 11	. . . . . . . 8
33		r1fin 8212	. . . . . . . . . 10
34		ficardom 8363	. . . . . . . . . 10
35	33, 34	syl 16	. . . . . . . . 9
36		ackbij2lem1 8620	. . . . . . . . 9
37	35, 36	syl 16	. . . . . . . 8
38		f1ores 5835	. . . . . . . 8
39	32, 37, 38	syl2anc 661	. . . . . . 7
40	30	ackbij1b 8640	. . . . . . . . . 10
41	35, 40	syl 16	. . . . . . . . 9
42		ficardid 8364	. . . . . . . . . 10
43		pwen 7710	. . . . . . . . . 10
44		carden2b 8369	. . . . . . . . . 10
45	33, 42, 43, 44	4syl 21	. . . . . . . . 9
46	41, 45	eqtrd 2498	. . . . . . . 8
47		f1oeq3 5814	. . . . . . . 8
48	46, 47	syl 16	. . . . . . 7
49	39, 48	mpbid 210	. . . . . 6
50	49	adantr 465	. . . . 5
51		f1opw 6529	. . . . . 6
52	51	adantl 466	. . . . 5
53		f1oco 5843	. . . . 5
54	50, 52, 53	syl2anc 661	. . . 4
55		frsuc 7121	. . . . . . . . 9
56		peano2 6720	. . . . . . . . . 10
57		fvres 5885	. . . . . . . . . 10
58	56, 57	syl 16	. . . . . . . . 9
59		fvres 5885	. . . . . . . . . . 11
60	59	fveq2d 5875	. . . . . . . . . 10
61		fvex 5881	. . . . . . . . . . 11
62		dmeq 5208	. . . . . . . . . . . . . 14
63	62	pweqd 4017	. . . . . . . . . . . . 13
64		imaeq1 5337	. . . . . . . . . . . . . 14
65	64	fveq2d 5875	. . . . . . . . . . . . 13
66	63, 65	mpteq12dv 4530	. . . . . . . . . . . 12
67		ackbij.g	. . . . . . . . . . . 12
68	61	dmex 6733	. . . . . . . . . . . . . 14
69	68	pwex 4635	. . . . . . . . . . . . 13
70	69	mptex 6143	. . . . . . . . . . . 12
71	66, 67, 70	fvmpt 5956	. . . . . . . . . . 11
72	61, 71	ax-mp 5	. . . . . . . . . 10
73	60, 72	syl6eq 2514	. . . . . . . . 9
74	55, 58, 73	3eqtr3d 2506	. . . . . . . 8
75	74	adantr 465	. . . . . . 7
76		f1odm 5825	. . . . . . . . . . 11
77	76	adantl 466	. . . . . . . . . 10
78	77	pweqd 4017	. . . . . . . . 9
79	78	mpteq1d 4533	. . . . . . . 8
80		fvex 5881	. . . . . . . . . . 11
81		eqid 2457	. . . . . . . . . . 11
82	80, 81	fnmpti 5714	. . . . . . . . . 10
83	82	a1i 11	. . . . . . . . 9
84		f1ofn 5822	. . . . . . . . . 10
85	54, 84	syl 16	. . . . . . . . 9
86		f1of 5821	. . . . . . . . . . . . . 14
87	52, 86	syl 16	. . . . . . . . . . . . 13
88	87	ffvelrnda 6031	. . . . . . . . . . . 12
89		fvres 5885	. . . . . . . . . . . 12
90	88, 89	syl 16	. . . . . . . . . . 11
91		imaeq2 5338	. . . . . . . . . . . . . 14
92		eqid 2457	. . . . . . . . . . . . . 14
93		imaexg 6737	. . . . . . . . . . . . . . 15
94	61, 93	ax-mp 5	. . . . . . . . . . . . . 14
95	91, 92, 94	fvmpt 5956	. . . . . . . . . . . . 13
96	95	adantl 466	. . . . . . . . . . . 12
97	96	fveq2d 5875	. . . . . . . . . . 11
98	90, 97	eqtrd 2498	. . . . . . . . . 10
99		fvco3 5950	. . . . . . . . . . 11
100	87, 99	sylan 471	. . . . . . . . . 10
101		imaeq2 5338	. . . . . . . . . . . . 13
102	101	fveq2d 5875	. . . . . . . . . . . 12
103		fvex 5881	. . . . . . . . . . . 12
104	102, 81, 103	fvmpt 5956	. . . . . . . . . . 11
105	104	adantl 466	. . . . . . . . . 10
106	98, 100, 105	3eqtr4rd 2509	. . . . . . . . 9
107	83, 85, 106	eqfnfvd 5984	. . . . . . . 8
108	79, 107	eqtrd 2498	. . . . . . 7
109	75, 108	eqtrd 2498	. . . . . 6
110		f1oeq1 5812	. . . . . 6
111	109, 110	syl 16	. . . . 5
112		nnon 6706	. . . . . . . 8
113		r1suc 8209	. . . . . . . 8
114	112, 113	syl 16	. . . . . . 7
115	114	fveq2d 5875	. . . . . . 7
116		f1oeq23 5815	. . . . . . 7
117	114, 115, 116	syl2anc 661	. . . . . 6
118	117	adantr 465	. . . . 5
119	111, 118	bitrd 253	. . . 4
120	54, 119	mpbird 232	. . 3
121	120	ex 434	. 2
122	4, 8, 12, 16, 29, 121	finds 6726	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  cvv 3109  i^icin 3474  C_wss 3475  c0 3784  ~Pcpw 4012  {csn 4029  U_ciun 4330   class class class wbr 4452  e.cmpt 4510  con0 4883  succsuc 4885  X.cxp 5002  domcdm 5004  |`cres 5006  "cima 5007  o.ccom 5008  Fnwfn 5588  -->wf 5589  -1-1->wf1 5590  -1-1-onto->wf1o 5592  `cfv 5593  com 6700  reccrdg 7094  cen 7533  cfn 7536  cr1 8201  ccrd 8337

This theorem is referenced by:  ackbij2lem3  8642  ackbij2  8644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-int 4287  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-1st 6800  df-2nd 6801  df-recs 7061  df-rdg 7095  df-1o 7149  df-2o 7150  df-oadd 7153  df-er 7330  df-map 7441  df-en 7537  df-dom 7538  df-sdom 7539  df-fin 7540  df-r1 8203  df-card 8341  df-cda 8569