funcpropd - Metamath Proof Explorer

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

Theorem funcpropd 16560

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same functors. (Contributed by Mario Carneiro, 17-Jan-2017.)

**Hypotheses**
Ref	Expression
funcpropd.1	_f _f
funcpropd.2	comp_f comp_f
funcpropd.3	_f _f
funcpropd.4	comp_f comp_f
funcpropd.a
funcpropd.b
funcpropd.c
funcpropd.d

**Assertion**
Ref	Expression
funcpropd

Proof of Theorem funcpropd Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relfunc 16522	. 2
2		relfunc 16522	. 2
3		funcpropd.1	. . . . . 6 _f _f
4		funcpropd.2	. . . . . 6 comp_f comp_f
5		funcpropd.a	. . . . . 6
6		funcpropd.b	. . . . . 6
7	3, 4, 5, 6	catpropd 16369	. . . . 5
8		funcpropd.3	. . . . . 6 _f _f
9		funcpropd.4	. . . . . 6 comp_f comp_f
10		funcpropd.c	. . . . . 6
11		funcpropd.d	. . . . . 6
12	8, 9, 10, 11	catpropd 16369	. . . . 5
13	7, 12	anbi12d 747	. . . 4 $/\$ $/\$
14		fveq2 6191	. . . . . . . . . . . . . 14
15	14	fveq2d 6195	. . . . . . . . . . . . 13
16		fveq2 6191	. . . . . . . . . . . . . 14
17	16	fveq2d 6195	. . . . . . . . . . . . 13
18	15, 17	oveq12d 6668	. . . . . . . . . . . 12
19		fveq2 6191	. . . . . . . . . . . 12
20	18, 19	oveq12d 6668	. . . . . . . . . . 11
21	20	cbvixpv 7926	. . . . . . . . . 10
22	21	eleq2i 2693	. . . . . . . . 9
23	22	anbi2i 730	. . . . . . . 8 $/\$ $/\$
24	3	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ _f _f
25	4	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ comp_f comp_f
26	5	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
27	6	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
28	24, 25, 26, 27	cidpropd 16370	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
29	28	fveq1d 6193	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
30	29	fveq2d 6195	. . . . . . . . . . 11 $/\$ $/\$ $/\$
31	8, 9, 10, 11	cidpropd 16370	. . . . . . . . . . . . 13
32	31	ad2antrr 762	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
33	32	fveq1d 6193	. . . . . . . . . . 11 $/\$ $/\$ $/\$
34	30, 33	eqeq12d 2637	. . . . . . . . . 10 $/\$ $/\$ $/\$
35		eqid 2622	. . . . . . . . . . . . . . . . . 18
36		eqid 2622	. . . . . . . . . . . . . . . . . 18
37		eqid 2622	. . . . . . . . . . . . . . . . . 18 comp comp
38		eqid 2622	. . . . . . . . . . . . . . . . . 18 comp comp
39	3	ad6antr 772	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
40	4	ad6antr 772	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp_f comp_f
41		simp-5r 809	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simp-4r 807	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43		simpllr 799	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44		simplr 792	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simpr 477	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45	comfeqval 16368	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
47	46	fveq2d 6195	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
48		eqid 2622	. . . . . . . . . . . . . . . . 17
49		eqid 2622	. . . . . . . . . . . . . . . . 17
50		eqid 2622	. . . . . . . . . . . . . . . . 17 comp comp
51		eqid 2622	. . . . . . . . . . . . . . . . 17 comp comp
52	8	ad6antr 772	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
53	9	ad6antr 772	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp_f comp_f
54		simprl 794	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
55	54	ad5antr 770	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55, 41	ffvelrnd 6360	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	55, 42	ffvelrnd 6360	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	55, 43	ffvelrnd 6360	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		df-ov 6653	. . . . . . . . . . . . . . . . . . . . 21
60		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
61	60	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
62	61	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp-4r 807	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65		opelxpi 5148	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
66	63, 64, 65	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
69	67, 68	op1std 7178	. . . . . . . . . . . . . . . . . . . . . . . . . 26
70	69	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25
71	67, 68	op2ndd 7179	. . . . . . . . . . . . . . . . . . . . . . . . . 26
72	71	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25
73	70, 72	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . 24
74		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25
75		df-ov 6653	. . . . . . . . . . . . . . . . . . . . . . . . 25
76	74, 75	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . . . . 24
77	73, 76	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . 23
78	77	fvixp 7913	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
79	62, 66, 78	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	59, 79	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81		elmapi 7879	. . . . . . . . . . . . . . . . . . . 20
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	82	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84	83, 44	ffvelrnd 6360	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		df-ov 6653	. . . . . . . . . . . . . . . . . . . . 21
86		opelxpi 5148	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
87	86	adantll 750	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
88		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
89	68, 88	op1std 7178	. . . . . . . . . . . . . . . . . . . . . . . . . 26
90	89	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25
91	68, 88	op2ndd 7179	. . . . . . . . . . . . . . . . . . . . . . . . . 26
92	91	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25
93	90, 92	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . 24
94		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		df-ov 6653	. . . . . . . . . . . . . . . . . . . . . . . . 25
96	94, 95	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . . . . 24
97	93, 96	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . 23
98	97	fvixp 7913	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
99	61, 87, 98	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
100	85, 99	syl5eqel 2705	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
101		elmapi 7879	. . . . . . . . . . . . . . . . . . . 20
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
103	102	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	103	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105	48, 49, 50, 51, 52, 53, 56, 57, 58, 84, 104	comfeqval 16368	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
106	47, 105	eqeq12d 2637	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
107	106	ralbidva 2985	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
108	107	ralbidva 2985	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
109		eqid 2622	. . . . . . . . . . . . . . 15
110	24	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
111		simpllr 799	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
112		simplr 792	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
113	35, 36, 109, 110, 111, 112	homfeqval 16357	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
114		simpr 477	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
115	35, 36, 109, 110, 112, 114	homfeqval 16357	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
116	115	raleqdv 3144	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
117	113, 116	raleqbidv 3152	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
118	108, 117	bitrd 268	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
119	118	ralbidva 2985	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ comp comp comp comp
120	119	ralbidva 2985	. . . . . . . . . 10 $/\$ $/\$ $/\$ comp comp comp comp
121	34, 120	anbi12d 747	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ comp comp $/\$ comp comp
122	121	ralbidva 2985	. . . . . . . 8 $/\$ $/\$ $/\$ comp comp $/\$ comp comp
123	23, 122	sylan2b 492	. . . . . . 7 $/\$ $/\$ $/\$ comp comp $/\$ comp comp
124	123	pm5.32da 673	. . . . . 6 $/\$ $/\$ $/\$ comp comp $/\$ $/\$ $/\$ comp comp
125		eqid 2622	. . . . . . . . . . . . . 14
126	8	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ _f _f
127		simplr 792	. . . . . . . . . . . . . . 15 $/\$ $/\$
128		xp1st 7198	. . . . . . . . . . . . . . . 16
129	128	adantl 482	. . . . . . . . . . . . . . 15 $/\$ $/\$
130	127, 129	ffvelrnd 6360	. . . . . . . . . . . . . 14 $/\$ $/\$
131		xp2nd 7199	. . . . . . . . . . . . . . . 16
132	131	adantl 482	. . . . . . . . . . . . . . 15 $/\$ $/\$
133	127, 132	ffvelrnd 6360	. . . . . . . . . . . . . 14 $/\$ $/\$
134	48, 49, 125, 126, 130, 133	homfeqval 16357	. . . . . . . . . . . . 13 $/\$ $/\$
135	3	ad2antrr 762	. . . . . . . . . . . . . . . 16 $/\$ $/\$ _f _f
136	35, 36, 109, 135, 129, 132	homfeqval 16357	. . . . . . . . . . . . . . 15 $/\$ $/\$
137		df-ov 6653	. . . . . . . . . . . . . . 15
138		df-ov 6653	. . . . . . . . . . . . . . 15
139	136, 137, 138	3eqtr3g 2679	. . . . . . . . . . . . . 14 $/\$ $/\$
140		1st2nd2 7205	. . . . . . . . . . . . . . . 16
141	140	adantl 482	. . . . . . . . . . . . . . 15 $/\$ $/\$
142	141	fveq2d 6195	. . . . . . . . . . . . . 14 $/\$ $/\$
143	141	fveq2d 6195	. . . . . . . . . . . . . 14 $/\$ $/\$
144	139, 142, 143	3eqtr4d 2666	. . . . . . . . . . . . 13 $/\$ $/\$
145	134, 144	oveq12d 6668	. . . . . . . . . . . 12 $/\$ $/\$
146	145	ixpeq2dva 7923	. . . . . . . . . . 11 $/\$
147	3	homfeqbas 16356	. . . . . . . . . . . . . 14
148	147	sqxpeqd 5141	. . . . . . . . . . . . 13
149	148	adantr 481	. . . . . . . . . . . 12 $/\$
150	149	ixpeq1d 7920	. . . . . . . . . . 11 $/\$
151	146, 150	eqtrd 2656	. . . . . . . . . 10 $/\$
152	151	eleq2d 2687	. . . . . . . . 9 $/\$
153	152	pm5.32da 673	. . . . . . . 8 $/\$ $/\$
154	8	homfeqbas 16356	. . . . . . . . . 10
155	147, 154	feq23d 6040	. . . . . . . . 9
156	155	anbi1d 741	. . . . . . . 8 $/\$ $/\$
157	153, 156	bitrd 268	. . . . . . 7 $/\$ $/\$
158	147	adantr 481	. . . . . . . . . 10 $/\$
159	158	raleqdv 3144	. . . . . . . . . 10 $/\$ comp comp comp comp
160	158, 159	raleqbidv 3152	. . . . . . . . 9 $/\$ comp comp comp comp
161	160	anbi2d 740	. . . . . . . 8 $/\$ $/\$ comp comp $/\$ comp comp
162	147, 161	raleqbidva 3154	. . . . . . 7 $/\$ comp comp $/\$ comp comp
163	157, 162	anbi12d 747	. . . . . 6 $/\$ $/\$ $/\$ comp comp $/\$ $/\$ $/\$ comp comp
164	124, 163	bitrd 268	. . . . 5 $/\$ $/\$ $/\$ comp comp $/\$ $/\$ $/\$ comp comp
165		df-3an 1039	. . . . 5 $/\$ $/\$ $/\$ comp comp $/\$ $/\$ $/\$ comp comp
166		df-3an 1039	. . . . 5 $/\$ $/\$ $/\$ comp comp $/\$ $/\$ $/\$ comp comp
167	164, 165, 166	3bitr4g 303	. . . 4 $/\$ $/\$ $/\$ comp comp $/\$ $/\$ $/\$ comp comp
168	13, 167	anbi12d 747	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
169		df-br 4654	. . . . 5
170		funcrcl 16523	. . . . 5 $/\$
171	169, 170	sylbi 207	. . . 4 $/\$
172		eqid 2622	. . . . 5
173		eqid 2622	. . . . 5
174		simpl 473	. . . . 5 $/\$
175		simpr 477	. . . . 5 $/\$
176	35, 48, 36, 49, 172, 173, 37, 50, 174, 175	isfunc 16524	. . . 4 $/\$ $/\$ $/\$ $/\$ comp comp
177	171, 176	biadan2 674	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
178		df-br 4654	. . . . 5
179		funcrcl 16523	. . . . 5 $/\$
180	178, 179	sylbi 207	. . . 4 $/\$
181		eqid 2622	. . . . 5
182		eqid 2622	. . . . 5
183		eqid 2622	. . . . 5
184		eqid 2622	. . . . 5
185		simpl 473	. . . . 5 $/\$
186		simpr 477	. . . . 5 $/\$
187	181, 182, 109, 125, 183, 184, 38, 51, 185, 186	isfunc 16524	. . . 4 $/\$ $/\$ $/\$ $/\$ comp comp
188	180, 187	biadan2 674	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
189	168, 177, 188	3bitr4g 303	. 2
190	1, 2, 189	eqbrrdiv 5218	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wral 2912

cop 4183 class class class wbr 4653

cxp 5112

wf 5884

cfv 5888 (class class class)co 6650

c1st 7166

c2nd 7167

cmap 7857

cixp 7908

cbs 15857

chom 15952 compcco 15953

ccat 16325

ccid 16326

_f chomf 16327 comp_fccomf 16328

cfunc 16514

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

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 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-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-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 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-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-1st 7168 df-2nd 7169 df-map 7859 df-ixp 7909 df-cat 16329 df-cid 16330 df-homf 16331 df-comf 16332 df-func 16518

This theorem is referenced by: funcres2c 16561 fullpropd 16580 fthpropd 16581 ressffth 16598 natpropd 16636 fucpropd 16637 funcsetcres2 16743

W3C validator