funcpropd - Metamath Proof Explorer

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

Theorem funcpropd 14052

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 14014	. 2
2		relfunc 14014	. 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 13890	. . . . 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 13890	. . . . 5
13	7, 12	anbi12d 692	. . . 4 $/\$ $/\$
14		fveq2 5687	. . . . . . . . . . . . . 14
15	14	fveq2d 5691	. . . . . . . . . . . . 13
16		fveq2 5687	. . . . . . . . . . . . . 14
17	16	fveq2d 5691	. . . . . . . . . . . . 13
18	15, 17	oveq12d 6058	. . . . . . . . . . . 12
19		fveq2 5687	. . . . . . . . . . . 12
20	18, 19	oveq12d 6058	. . . . . . . . . . 11
21	20	cbvixpv 7039	. . . . . . . . . 10
22	21	eleq2i 2468	. . . . . . . . 9
23	22	anbi2i 676	. . . . . . . 8 $/\$ $/\$
24	3	ad2antrr 707	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ _f _f
25	4	ad2antrr 707	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ comp_f comp_f
26	5	ad2antrr 707	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
27	6	ad2antrr 707	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
28	24, 25, 26, 27	cidpropd 13891	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
29	28	fveq1d 5689	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
30	29	fveq2d 5691	. . . . . . . . . . 11 $/\$ $/\$ $/\$
31	8, 9, 10, 11	cidpropd 13891	. . . . . . . . . . . . 13
32	31	ad2antrr 707	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
33	32	fveq1d 5689	. . . . . . . . . . 11 $/\$ $/\$ $/\$
34	30, 33	eqeq12d 2418	. . . . . . . . . 10 $/\$ $/\$ $/\$
35		eqid 2404	. . . . . . . . . . . . . . . . . 18
36		eqid 2404	. . . . . . . . . . . . . . . . . 18
37		eqid 2404	. . . . . . . . . . . . . . . . . 18 comp comp
38		eqid 2404	. . . . . . . . . . . . . . . . . 18 comp comp
39	3	ad6antr 717	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
40	4	ad6antr 717	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp_f comp_f
41		simp-5r 746	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simp-4r 744	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43		simpllr 736	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44		simplr 732	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simpr 448	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45	comfeqval 13889	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
47	46	fveq2d 5691	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
48		eqid 2404	. . . . . . . . . . . . . . . . 17
49		eqid 2404	. . . . . . . . . . . . . . . . 17
50		eqid 2404	. . . . . . . . . . . . . . . . 17 comp comp
51		eqid 2404	. . . . . . . . . . . . . . . . 17 comp comp
52	8	ad6antr 717	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
53	9	ad6antr 717	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp_f comp_f
54		simprl 733	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
55	54	ad5antr 715	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55, 41	ffvelrnd 5830	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	55, 42	ffvelrnd 5830	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	55, 43	ffvelrnd 5830	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		df-ov 6043	. . . . . . . . . . . . . . . . . . . . 21
60		simprr 734	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
61	60	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
62	61	adantr 452	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp-4r 744	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		simpllr 736	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65		opelxpi 4869	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
66	63, 64, 65	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67		vex 2919	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68		vex 2919	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
69	67, 68	op1std 6316	. . . . . . . . . . . . . . . . . . . . . . . . . 26
70	69	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . . 25
71	67, 68	op2ndd 6317	. . . . . . . . . . . . . . . . . . . . . . . . . 26
72	71	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . . 25
73	70, 72	oveq12d 6058	. . . . . . . . . . . . . . . . . . . . . . . 24
74		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . 25
75		df-ov 6043	. . . . . . . . . . . . . . . . . . . . . . . . 25
76	74, 75	syl6eqr 2454	. . . . . . . . . . . . . . . . . . . . . . . 24
77	73, 76	oveq12d 6058	. . . . . . . . . . . . . . . . . . . . . . 23
78	77	fvixp 7026	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
79	62, 66, 78	syl2anc 643	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	59, 79	syl5eqel 2488	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81		elmapi 6997	. . . . . . . . . . . . . . . . . . . 20
82	80, 81	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	82	adantr 452	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84	83, 44	ffvelrnd 5830	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		df-ov 6043	. . . . . . . . . . . . . . . . . . . . 21
86		opelxpi 4869	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
87	86	adantll 695	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
88		vex 2919	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
89	68, 88	op1std 6316	. . . . . . . . . . . . . . . . . . . . . . . . . 26
90	89	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . . 25
91	68, 88	op2ndd 6317	. . . . . . . . . . . . . . . . . . . . . . . . . 26
92	91	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . . 25
93	90, 92	oveq12d 6058	. . . . . . . . . . . . . . . . . . . . . . . 24
94		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		df-ov 6043	. . . . . . . . . . . . . . . . . . . . . . . . 25
96	94, 95	syl6eqr 2454	. . . . . . . . . . . . . . . . . . . . . . . 24
97	93, 96	oveq12d 6058	. . . . . . . . . . . . . . . . . . . . . . 23
98	97	fvixp 7026	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
99	61, 87, 98	syl2anc 643	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
100	85, 99	syl5eqel 2488	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
101		elmapi 6997	. . . . . . . . . . . . . . . . . . . 20
102	100, 101	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
103	102	adantr 452	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	103	ffvelrnda 5829	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105	48, 49, 50, 51, 52, 53, 56, 57, 58, 84, 104	comfeqval 13889	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
106	47, 105	eqeq12d 2418	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
107	106	ralbidva 2682	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
108	107	ralbidva 2682	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
109		eqid 2404	. . . . . . . . . . . . . . 15
110	24	ad2antrr 707	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
111		simpllr 736	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
112		simplr 732	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
113	35, 36, 109, 110, 111, 112	homfeqval 13878	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
114		simpr 448	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
115	35, 36, 109, 110, 112, 114	homfeqval 13878	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
116	115	raleqdv 2870	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
117	113, 116	raleqbidv 2876	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
118	108, 117	bitrd 245	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
119	118	ralbidva 2682	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ comp comp comp comp
120	119	ralbidva 2682	. . . . . . . . . 10 $/\$ $/\$ $/\$ comp comp comp comp
121	34, 120	anbi12d 692	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ comp comp $/\$ comp comp
122	121	ralbidva 2682	. . . . . . . 8 $/\$ $/\$ $/\$ comp comp $/\$ comp comp
123	23, 122	sylan2b 462	. . . . . . 7 $/\$ $/\$ $/\$ comp comp $/\$ comp comp
124	123	pm5.32da 623	. . . . . 6 $/\$ $/\$ $/\$ comp comp $/\$ $/\$ $/\$ comp comp
125		eqid 2404	. . . . . . . . . . . . . 14
126	8	ad2antrr 707	. . . . . . . . . . . . . 14 $/\$ $/\$ _f _f
127		simplr 732	. . . . . . . . . . . . . . 15 $/\$ $/\$
128		xp1st 6335	. . . . . . . . . . . . . . . 16
129	128	adantl 453	. . . . . . . . . . . . . . 15 $/\$ $/\$
130	127, 129	ffvelrnd 5830	. . . . . . . . . . . . . 14 $/\$ $/\$
131		xp2nd 6336	. . . . . . . . . . . . . . . 16
132	131	adantl 453	. . . . . . . . . . . . . . 15 $/\$ $/\$
133	127, 132	ffvelrnd 5830	. . . . . . . . . . . . . 14 $/\$ $/\$
134	48, 49, 125, 126, 130, 133	homfeqval 13878	. . . . . . . . . . . . 13 $/\$ $/\$
135	3	ad2antrr 707	. . . . . . . . . . . . . . . 16 $/\$ $/\$ _f _f
136	35, 36, 109, 135, 129, 132	homfeqval 13878	. . . . . . . . . . . . . . 15 $/\$ $/\$
137		df-ov 6043	. . . . . . . . . . . . . . 15
138		df-ov 6043	. . . . . . . . . . . . . . 15
139	136, 137, 138	3eqtr3g 2459	. . . . . . . . . . . . . 14 $/\$ $/\$
140		1st2nd2 6345	. . . . . . . . . . . . . . . 16
141	140	adantl 453	. . . . . . . . . . . . . . 15 $/\$ $/\$
142	141	fveq2d 5691	. . . . . . . . . . . . . 14 $/\$ $/\$
143	141	fveq2d 5691	. . . . . . . . . . . . . 14 $/\$ $/\$
144	139, 142, 143	3eqtr4d 2446	. . . . . . . . . . . . 13 $/\$ $/\$
145	134, 144	oveq12d 6058	. . . . . . . . . . . 12 $/\$ $/\$
146	145	ixpeq2dva 7036	. . . . . . . . . . 11 $/\$
147	3	homfeqbas 13877	. . . . . . . . . . . . . 14
148	147, 147	xpeq12d 4862	. . . . . . . . . . . . 13
149	148	adantr 452	. . . . . . . . . . . 12 $/\$
150	149	ixpeq1d 7033	. . . . . . . . . . 11 $/\$
151	146, 150	eqtrd 2436	. . . . . . . . . 10 $/\$
152	151	eleq2d 2471	. . . . . . . . 9 $/\$
153	152	pm5.32da 623	. . . . . . . 8 $/\$ $/\$
154	8	homfeqbas 13877	. . . . . . . . . 10
155	147, 154	feq23d 5547	. . . . . . . . 9
156	155	anbi1d 686	. . . . . . . 8 $/\$ $/\$
157	153, 156	bitrd 245	. . . . . . 7 $/\$ $/\$
158	147	adantr 452	. . . . . . . . . 10 $/\$
159	158	raleqdv 2870	. . . . . . . . . 10 $/\$ comp comp comp comp
160	158, 159	raleqbidv 2876	. . . . . . . . 9 $/\$ comp comp comp comp
161	160	anbi2d 685	. . . . . . . 8 $/\$ $/\$ comp comp $/\$ comp comp
162	147, 161	raleqbidva 2878	. . . . . . 7 $/\$ comp comp $/\$ comp comp
163	157, 162	anbi12d 692	. . . . . 6 $/\$ $/\$ $/\$ comp comp $/\$ $/\$ $/\$ comp comp
164	124, 163	bitrd 245	. . . . 5 $/\$ $/\$ $/\$