funcpropd - Metamath Proof Explorer

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

Theorem funcpropd 15138

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 15100	. 2
2		relfunc 15100	. 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 14976	. . . . 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 14976	. . . . 5
13	7, 12	anbi12d 710	. . . 4 $/\$ $/\$
14		fveq2 5852	. . . . . . . . . . . . . 14
15	14	fveq2d 5856	. . . . . . . . . . . . 13
16		fveq2 5852	. . . . . . . . . . . . . 14
17	16	fveq2d 5856	. . . . . . . . . . . . 13
18	15, 17	oveq12d 6295	. . . . . . . . . . . 12
19		fveq2 5852	. . . . . . . . . . . 12
20	18, 19	oveq12d 6295	. . . . . . . . . . 11
21	20	cbvixpv 7485	. . . . . . . . . 10
22	21	eleq2i 2519	. . . . . . . . 9
23	22	anbi2i 694	. . . . . . . 8 $/\$ $/\$
24	3	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ _f _f
25	4	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ comp_f comp_f
26	5	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
27	6	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
28	24, 25, 26, 27	cidpropd 14977	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
29	28	fveq1d 5854	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
30	29	fveq2d 5856	. . . . . . . . . . 11 $/\$ $/\$ $/\$
31	8, 9, 10, 11	cidpropd 14977	. . . . . . . . . . . . 13
32	31	ad2antrr 725	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
33	32	fveq1d 5854	. . . . . . . . . . 11 $/\$ $/\$ $/\$
34	30, 33	eqeq12d 2463	. . . . . . . . . 10 $/\$ $/\$ $/\$
35		eqid 2441	. . . . . . . . . . . . . . . . . 18
36		eqid 2441	. . . . . . . . . . . . . . . . . 18
37		eqid 2441	. . . . . . . . . . . . . . . . . 18 comp comp
38		eqid 2441	. . . . . . . . . . . . . . . . . 18 comp comp
39	3	ad6antr 735	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
40	4	ad6antr 735	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp_f comp_f
41		simp-5r 768	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simp-4r 766	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43		simpllr 758	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44		simplr 754	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simpr 461	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45	comfeqval 14975	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
47	46	fveq2d 5856	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
48		eqid 2441	. . . . . . . . . . . . . . . . 17
49		eqid 2441	. . . . . . . . . . . . . . . . 17
50		eqid 2441	. . . . . . . . . . . . . . . . 17 comp comp
51		eqid 2441	. . . . . . . . . . . . . . . . 17 comp comp
52	8	ad6antr 735	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
53	9	ad6antr 735	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp_f comp_f
54		simprl 755	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
55	54	ad5antr 733	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55, 41	ffvelrnd 6013	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	55, 42	ffvelrnd 6013	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	55, 43	ffvelrnd 6013	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		df-ov 6280	. . . . . . . . . . . . . . . . . . . . 21
60		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
61	60	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
62	61	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp-4r 766	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		simpllr 758	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65		opelxpi 5017	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
66	63, 64, 65	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67		vex 3096	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68		vex 3096	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
69	67, 68	op1std 6791	. . . . . . . . . . . . . . . . . . . . . . . . . 26
70	69	fveq2d 5856	. . . . . . . . . . . . . . . . . . . . . . . . 25
71	67, 68	op2ndd 6792	. . . . . . . . . . . . . . . . . . . . . . . . . 26
72	71	fveq2d 5856	. . . . . . . . . . . . . . . . . . . . . . . . 25
73	70, 72	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . . . 24
74		fveq2 5852	. . . . . . . . . . . . . . . . . . . . . . . . 25
75		df-ov 6280	. . . . . . . . . . . . . . . . . . . . . . . . 25
76	74, 75	syl6eqr 2500	. . . . . . . . . . . . . . . . . . . . . . . 24
77	73, 76	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . . 23
78	77	fvixp 7472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
79	62, 66, 78	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	59, 79	syl5eqel 2533	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81		elmapi 7438	. . . . . . . . . . . . . . . . . . . 20
82	80, 81	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	82	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84	83, 44	ffvelrnd 6013	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		df-ov 6280	. . . . . . . . . . . . . . . . . . . . 21
86		opelxpi 5017	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
87	86	adantll 713	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
88		vex 3096	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
89	68, 88	op1std 6791	. . . . . . . . . . . . . . . . . . . . . . . . . 26
90	89	fveq2d 5856	. . . . . . . . . . . . . . . . . . . . . . . . 25
91	68, 88	op2ndd 6792	. . . . . . . . . . . . . . . . . . . . . . . . . 26
92	91	fveq2d 5856	. . . . . . . . . . . . . . . . . . . . . . . . 25
93	90, 92	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . . . 24
94		fveq2 5852	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		df-ov 6280	. . . . . . . . . . . . . . . . . . . . . . . . 25
96	94, 95	syl6eqr 2500	. . . . . . . . . . . . . . . . . . . . . . . 24
97	93, 96	oveq12d 6295	. . . . . . . . . . . . . . . . . . . . . . 23
98	97	fvixp 7472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
99	61, 87, 98	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
100	85, 99	syl5eqel 2533	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
101		elmapi 7438	. . . . . . . . . . . . . . . . . . . 20
102	100, 101	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
103	102	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	103	ffvelrnda 6012	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105	48, 49, 50, 51, 52, 53, 56, 57, 58, 84, 104	comfeqval 14975	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
106	47, 105	eqeq12d 2463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
107	106	ralbidva 2877	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
108	107	ralbidva 2877	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
109		eqid 2441	. . . . . . . . . . . . . . 15
110	24	ad2antrr 725	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
111		simpllr 758	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
112		simplr 754	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
113	35, 36, 109, 110, 111, 112	homfeqval 14964	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
114		simpr 461	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
115	35, 36, 109, 110, 112, 114	homfeqval 14964	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
116	115	raleqdv 3044	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
117	113, 116	raleqbidv 3052	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
118	108, 117	bitrd 253	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
119	118	ralbidva 2877	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ comp comp comp comp
120	119	ralbidva 2877	. . . . . . . . . 10 $/\$ $/\$ $/\$ comp comp comp comp
121	34, 120	anbi12d 710	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ comp comp $/\$ comp comp
122	121	ralbidva 2877	. . . . . . . 8 $/\$ $/\$ $/\$ comp comp $/\$ comp comp
123	23, 122	sylan2b 475	. . . . . . 7 $/\$ $/\$ $/\$ comp comp $/\$ comp comp
124	123	pm5.32da 641	. . . . . 6 $/\$ $/\$ $/\$ comp comp $/\$ $/\$ $/\$ comp comp
125		eqid 2441	. . . . . . . . . . . . . 14
126	8	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ _f _f
127		simplr 754	. . . . . . . . . . . . . . 15 $/\$ $/\$
128		xp1st 6811	. . . . . . . . . . . . . . . 16
129	128	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$
130	127, 129	ffvelrnd 6013	. . . . . . . . . . . . . 14 $/\$ $/\$
131		xp2nd 6812	. . . . . . . . . . . . . . . 16
132	131	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$
133	127, 132	ffvelrnd 6013	. . . . . . . . . . . . . 14 $/\$ $/\$
134	48, 49, 125, 126, 130, 133	homfeqval 14964	. . . . . . . . . . . . 13 $/\$ $/\$
135	3	ad2antrr 725	. . . . . . . . . . . . . . . 16 $/\$ $/\$ _f _f
136	35, 36, 109, 135, 129, 132	homfeqval 14964	. . . . . . . . . . . . . . 15 $/\$ $/\$
137		df-ov 6280	. . . . . . . . . . . . . . 15
138		df-ov 6280	. . . . . . . . . . . . . . 15
139	136, 137, 138	3eqtr3g 2505	. . . . . . . . . . . . . 14 $/\$ $/\$
140		1st2nd2 6818	. . . . . . . . . . . . . . . 16
141	140	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$
142	141	fveq2d 5856	. . . . . . . . . . . . . 14 $/\$ $/\$
143	141	fveq2d 5856	. . . . . . . . . . . . . 14 $/\$ $/\$
144	139, 142, 143	3eqtr4d 2492	. . . . . . . . . . . . 13 $/\$ $/\$
145	134, 144	oveq12d 6295	. . . . . . . . . . . 12 $/\$ $/\$
146	145	ixpeq2dva 7482	. . . . . . . . . . 11 $/\$
147	3	homfeqbas 14963	. . . . . . . . . . . . . 14
148	147	sqxpeqd 5011	. . . . . . . . . . . . 13
149	148	adantr 465	. . . . . . . . . . . 12 $/\$
150	149	ixpeq1d 7479	. . . . . . . . . . 11 $/\$
151	146, 150	eqtrd 2482	. . . . . . . . . 10 $/\$
152	151	eleq2d 2511	. . . . . . . . 9 $/\$
153	152	pm5.32da 641	. . . . . . . 8 $/\$ $/\$
154	8	homfeqbas 14963	. . . . . . . . . 10
155	147, 154	feq23d 5712	. . . . . . . . 9
156	155	anbi1d 704	. . . . . . . 8 $/\$ $/\$
157	153, 156	bitrd 253	. . . . . . 7 $/\$ $/\$
158	147	adantr 465	. . . . . . . . . 10 $/\$
159	158	raleqdv 3044	. . . . . . . . . 10 $/\$ comp comp comp comp
160	158, 159	raleqbidv 3052	. . . . . . . . 9 $/\$ comp comp comp comp
161	160	anbi2d 703	. . . . . . . 8 $/\$ $/\$ comp comp $/\$ comp comp
162	147, 161	raleqbidva 3054	. . . . . . 7 $/\$ comp comp $/\$ comp comp
163	157, 162	anbi12d 710	. . . . . 6 $/\$ $/\$ $/\$ comp comp $/\$ $/\$ $/\$ comp comp
164	124, 163	bitrd 253	. . . . 5 $/\$ $/\$ $/\$