cofucl - Metamath Proof Explorer

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

Theorem cofucl 14783

Description: The composition of two functors is a functor. (Contributed by Mario Carneiro, 3-Jan-2017.)

**Hypotheses**
Ref	Expression
cofucl.f
cofucl.g

**Assertion**
Ref	Expression
cofucl	_func

Proof of Theorem cofucl Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2435	. . . 4
2		cofucl.f	. . . 4
3		cofucl.g	. . . 4
4	1, 2, 3	cofuval 14777	. . 3 _func
5	1, 2, 3	cofu1st 14778	. . . 4 _func
6	4	fveq2d 5685	. . . . 5 _func
7		fvex 5691	. . . . . . 7
8		fvex 5691	. . . . . . 7
9	7, 8	coex 6520	. . . . . 6
10		fvex 5691	. . . . . . 7
11	10, 10	mpt2ex 6641	. . . . . 6
12	9, 11	op2nd 6577	. . . . 5
13	6, 12	syl6eq 2483	. . . 4 _func
14	5, 13	opeq12d 4057	. . 3 _func _func
15	4, 14	eqtr4d 2470	. 2 _func _func _func
16		eqid 2435	. . . . . . 7
17		eqid 2435	. . . . . . 7
18		relfunc 14757	. . . . . . . 8
19		1st2ndbr 6614	. . . . . . . 8 $/\$
20	18, 3, 19	sylancr 658	. . . . . . 7
21	16, 17, 20	funcf1 14761	. . . . . 6
22		relfunc 14757	. . . . . . . 8
23		1st2ndbr 6614	. . . . . . . 8 $/\$
24	22, 2, 23	sylancr 658	. . . . . . 7
25	1, 16, 24	funcf1 14761	. . . . . 6
26		fco 5558	. . . . . 6 $/\$
27	21, 25, 26	syl2anc 656	. . . . 5
28	5	feq1d 5536	. . . . 5 _func
29	27, 28	mpbird 232	. . . 4 _func
30		eqid 2435	. . . . . . 7
31		ovex 6107	. . . . . . . 8
32		ovex 6107	. . . . . . . 8
33	31, 32	coex 6520	. . . . . . 7
34	30, 33	fnmpt2i 6634	. . . . . 6
35	13	fneq1d 5491	. . . . . 6 _func
36	34, 35	mpbiri 233	. . . . 5 _func
37		eqid 2435	. . . . . . . . . . 11
38		eqid 2435	. . . . . . . . . . 11
39	20	adantr 462	. . . . . . . . . . 11 $/\$ $/\$
40	25	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$
41		simprl 750	. . . . . . . . . . . 12 $/\$ $/\$
42	40, 41	ffvelrnd 5834	. . . . . . . . . . 11 $/\$ $/\$
43		simprr 751	. . . . . . . . . . . 12 $/\$ $/\$
44	40, 43	ffvelrnd 5834	. . . . . . . . . . 11 $/\$ $/\$
45	16, 37, 38, 39, 42, 44	funcf2 14763	. . . . . . . . . 10 $/\$ $/\$
46		eqid 2435	. . . . . . . . . . 11
47	24	adantr 462	. . . . . . . . . . 11 $/\$ $/\$
48	1, 46, 37, 47, 41, 43	funcf2 14763	. . . . . . . . . 10 $/\$ $/\$
49		fco 5558	. . . . . . . . . 10 $/\$
50	45, 48, 49	syl2anc 656	. . . . . . . . 9 $/\$ $/\$
51		ovex 6107	. . . . . . . . . 10
52		ovex 6107	. . . . . . . . . 10
53	51, 52	elmap 7231	. . . . . . . . 9
54	50, 53	sylibr 212	. . . . . . . 8 $/\$ $/\$
55	2	adantr 462	. . . . . . . . 9 $/\$ $/\$
56	3	adantr 462	. . . . . . . . 9 $/\$ $/\$
57	1, 55, 56, 41, 43	cofu2nd 14780	. . . . . . . 8 $/\$ $/\$ _func
58	1, 55, 56, 41	cofu1 14779	. . . . . . . . . 10 $/\$ $/\$ _func
59	1, 55, 56, 43	cofu1 14779	. . . . . . . . . 10 $/\$ $/\$ _func
60	58, 59	oveq12d 6100	. . . . . . . . 9 $/\$ $/\$ _func _func
61	60	oveq1d 6097	. . . . . . . 8 $/\$ $/\$ _func _func
62	54, 57, 61	3eltr4d 2516	. . . . . . 7 $/\$ $/\$ _func _func _func
63	62	ralrimivva 2800	. . . . . 6 _func _func _func
64		fveq2 5681	. . . . . . . . 9 _func _func
65		df-ov 6085	. . . . . . . . 9 _func _func
66	64, 65	syl6eqr 2485	. . . . . . . 8 _func _func
67		vex 2967	. . . . . . . . . . . 12
68		vex 2967	. . . . . . . . . . . 12
69	67, 68	op1std 6578	. . . . . . . . . . 11
70	69	fveq2d 5685	. . . . . . . . . 10 _func _func
71	67, 68	op2ndd 6579	. . . . . . . . . . 11
72	71	fveq2d 5685	. . . . . . . . . 10 _func _func
73	70, 72	oveq12d 6100	. . . . . . . . 9 _func _func _func _func
74		fveq2 5681	. . . . . . . . . 10
75		df-ov 6085	. . . . . . . . . 10
76	74, 75	syl6eqr 2485	. . . . . . . . 9
77	73, 76	oveq12d 6100	. . . . . . . 8 _func _func _func _func
78	66, 77	eleq12d 2503	. . . . . . 7 _func _func _func _func _func _func
79	78	ralxp 4970	. . . . . 6 _func _func _func _func _func _func
80	63, 79	sylibr 212	. . . . 5 _func _func _func
81		fvex 5691	. . . . . 6 _func
82	81	elixp 7260	. . . . 5 _func _func _func _func $/\$ _func _func _func
83	36, 80, 82	sylanbrc 659	. . . 4 _func _func _func
84		eqid 2435	. . . . . . . . . 10
85		eqid 2435	. . . . . . . . . 10
86	24	adantr 462	. . . . . . . . . 10 $/\$
87		simpr 458	. . . . . . . . . 10 $/\$
88	1, 84, 85, 86, 87	funcid 14765	. . . . . . . . 9 $/\$
89	88	fveq2d 5685	. . . . . . . 8 $/\$
90		eqid 2435	. . . . . . . . 9
91	20	adantr 462	. . . . . . . . 9 $/\$
92	25	ffvelrnda 5833	. . . . . . . . 9 $/\$
93	16, 85, 90, 91, 92	funcid 14765	. . . . . . . 8 $/\$
94	89, 93	eqtrd 2467	. . . . . . 7 $/\$
95	2	adantr 462	. . . . . . . 8 $/\$
96	3	adantr 462	. . . . . . . 8 $/\$
97		funcrcl 14758	. . . . . . . . . . . 12 $/\$
98	2, 97	syl 16	. . . . . . . . . . 11 $/\$
99	98	simpld 456	. . . . . . . . . 10
100	99	adantr 462	. . . . . . . . 9 $/\$
101	1, 46, 84, 100, 87	catidcl 14605	. . . . . . . 8 $/\$
102	1, 95, 96, 87, 87, 46, 101	cofu2 14781	. . . . . . 7 $/\$ _func
103	1, 95, 96, 87	cofu1 14779	. . . . . . . 8 $/\$ _func
104	103	fveq2d 5685	. . . . . . 7 $/\$ _func
105	94, 102, 104	3eqtr4d 2477	. . . . . 6 $/\$ _func _func
106	86	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
107		simplr 749	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
108		simprlr 757	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
109	1, 46, 37, 106, 107, 108	funcf2 14763	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
110		eqid 2435	. . . . . . . . . . . . 13 comp comp
111	100	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
112		simprll 756	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
113		simprrl 758	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
114		simprrr 759	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
115	1, 46, 110, 111, 107, 112, 108, 113, 114	catcocl 14608	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ comp
116		fvco3 5758	. . . . . . . . . . . 12 $/\$ comp comp comp
117	109, 115, 116	syl2anc 656	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
118		eqid 2435	. . . . . . . . . . . . 13 comp comp
119	1, 46, 110, 118, 106, 107, 112, 108, 113, 114	funcco 14766	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
120	119	fveq2d 5685	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
121		eqid 2435	. . . . . . . . . . . 12 comp comp
122	91	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
123	92	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
124	25	adantr 462	. . . . . . . . . . . . . 14 $/\$
125	124	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
126	125, 112	ffvelrnd 5834	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
127	125, 108	ffvelrnd 5834	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
128	1, 46, 37, 106, 107, 112	funcf2 14763	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
129	128, 113	ffvelrnd 5834	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
130	1, 46, 37, 106, 112, 108	funcf2 14763	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
131	130, 114	ffvelrnd 5834	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
132	16, 37, 118, 121, 122, 123, 126, 127, 129, 131	funcco 14766	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
133	117, 120, 132	3eqtrd 2471	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
134	95	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
135	96	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
136	1, 134, 135, 107, 108	cofu2nd 14780	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ _func
137	136	fveq1d 5683	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ _func comp comp
138	103	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ _func
139	1, 134, 135, 112	cofu1 14779	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ _func
140	138, 139	opeq12d 4057	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ _func _func
141	1, 134, 135, 108	cofu1 14779	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ _func
142	140, 141	oveq12d 6100	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ _func _func comp _func comp
143	1, 134, 135, 112, 108, 46, 114	cofu2 14781	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ _func
144	1, 134, 135, 107, 112, 46, 113	cofu2 14781	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ _func
145	142, 143, 144	oveq123d 6103	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ _func _func _func comp _func _func comp
146	133, 137, 145	3eqtr4d 2477	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ _func comp _func _func _func comp _func _func
147	146	anassrs 643	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ _func comp _func _func _func comp _func _func
148	147	ralrimivva 2800	. . . . . . 7 $/\$ $/\$ $/\$ _func comp _func _func _func comp _func _func
149	148	ralrimivva 2800	. . . . . 6 $/\$ _func comp _func _func _func comp _func _func
150	105, 149	jca 529	. . . . 5 $/\$ _func _func $/\$ _func comp _func _func _func comp _func _func
151	150	ralrimiva 2791	. . . 4 _func _func $/\$ _func comp _func _func _func comp _func _func
152		funcrcl 14758	. . . . . . 7 $/\$
153	3, 152	syl 16	. . . . . 6 $/\$
154	153	simprd 460	. . . . 5
155	1, 17, 46, 38, 84, 90, 110, 121, 99, 154	isfunc 14759	. . . 4 _func _func _func $/\$ _func _func _func $/\$ _func _func $/\$ _func comp _func _func _func comp _func _func
156	29, 83, 151, 155	mpbir3and 1166	. . 3 _func _func
157		df-br 4283	. . 3 _func _func _func _func
158	156, 157	sylib 196	. 2 _func _func
159	15, 158	eqeltrd 2509	1 _func

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369

wceq 1364

wcel 1757

wral 2707

cop 3873 class class class wbr 4282

cxp 4827

ccom 4833

wrel 4834

wfn 5403

wf 5404

cfv 5408 (class class class)co 6082

cmpt2 6084

c1st 6566

c2nd 6567

cmap 7204

cixp 7253

cbs 14159

chom 14234 compcco 14235

ccat 14587

ccid 14588

cfunc 14749

_func ccofu 14751

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1671 ax-6 1709 ax-7 1729 ax-8 1759 ax-9 1761 ax-10 1776 ax-11 1781 ax-12 1793 ax-13 1944 ax-ext 2416 ax-rep 4393 ax-sep 4403 ax-nul 4411 ax-pow 4460 ax-pr 4521 ax-un 6363

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1702 df-eu 2260 df-mo 2261 df-clab 2422 df-cleq 2428 df-clel 2431 df-nfc 2560 df-ne 2600 df-ral 2712 df-rex 2713 df-reu 2714 df-rmo 2715 df-rab 2716 df-v 2966 df-sbc 3178 df-csb 3279 df-dif 3321 df-un 3323 df-in 3325 df-ss 3332 df-nul 3628 df-if 3782 df-pw 3852 df-sn 3868 df-pr 3870 df-op 3874 df-uni 4082 df-iun 4163 df-br 4283 df-opab 4341 df-mpt 4342 df-id 4625 df-xp 4835 df-rel 4836 df-cnv 4837 df-co 4838 df-dm 4839 df-rn 4840 df-res 4841 df-ima 4842 df-iota 5371 df-fun 5410 df-fn 5411 df-f 5412 df-f1 5413 df-fo 5414 df-f1o 5415 df-fv 5416 df-riota 6041 df-ov 6085 df-oprab 6086 df-mpt2 6087 df-1st 6568 df-2nd 6569 df-map 7206 df-ixp 7254 df-cat 14591 df-cid 14592 df-func 14753 df-cofu 14755

This theorem is referenced by: cofuass 14784 cofull 14829 cofth 14830 catccatid 14955 1st2ndprf 15001 uncfcl 15030 uncf1 15031 uncf2 15032 yonedalem1 15067 yonedalem21 15068 yonedalem22 15073

W3C validator