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 15860

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 15822	. 2
2		relfunc 15822	. 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 15669	. . . . 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 15669	. . . . 5
13	7, 12	anbi12d 722	. . . 4 $/\$ $/\$
14		fveq2 5892	. . . . . . . . . . . . . 14
15	14	fveq2d 5896	. . . . . . . . . . . . 13
16		fveq2 5892	. . . . . . . . . . . . . 14
17	16	fveq2d 5896	. . . . . . . . . . . . 13
18	15, 17	oveq12d 6338	. . . . . . . . . . . 12
19		fveq2 5892	. . . . . . . . . . . 12
20	18, 19	oveq12d 6338	. . . . . . . . . . 11
21	20	cbvixpv 7571	. . . . . . . . . 10
22	21	eleq2i 2532	. . . . . . . . 9
23	22	anbi2i 705	. . . . . . . 8 $/\$ $/\$
24	3	ad2antrr 737	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ _f _f
25	4	ad2antrr 737	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ comp_f comp_f
26	5	ad2antrr 737	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
27	6	ad2antrr 737	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
28	24, 25, 26, 27	cidpropd 15670	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
29	28	fveq1d 5894	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
30	29	fveq2d 5896	. . . . . . . . . . 11 $/\$ $/\$ $/\$
31	8, 9, 10, 11	cidpropd 15670	. . . . . . . . . . . . 13
32	31	ad2antrr 737	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
33	32	fveq1d 5894	. . . . . . . . . . 11 $/\$ $/\$ $/\$
34	30, 33	eqeq12d 2477	. . . . . . . . . 10 $/\$ $/\$ $/\$
35		eqid 2462	. . . . . . . . . . . . . . . . . 18
36		eqid 2462	. . . . . . . . . . . . . . . . . 18
37		eqid 2462	. . . . . . . . . . . . . . . . . 18 comp comp
38		eqid 2462	. . . . . . . . . . . . . . . . . 18 comp comp
39	3	ad6antr 747	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
40	4	ad6antr 747	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp_f comp_f
41		simp-5r 784	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simp-4r 782	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43		simpllr 774	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44		simplr 767	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simpr 467	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45	comfeqval 15668	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
47	46	fveq2d 5896	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
48		eqid 2462	. . . . . . . . . . . . . . . . 17
49		eqid 2462	. . . . . . . . . . . . . . . . 17
50		eqid 2462	. . . . . . . . . . . . . . . . 17 comp comp
51		eqid 2462	. . . . . . . . . . . . . . . . 17 comp comp
52	8	ad6antr 747	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
53	9	ad6antr 747	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp_f comp_f
54		simprl 769	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
55	54	ad5antr 745	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	55, 41	ffvelrnd 6051	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	55, 42	ffvelrnd 6051	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	55, 43	ffvelrnd 6051	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59		df-ov 6323	. . . . . . . . . . . . . . . . . . . . 21
60		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
61	60	ad3antrrr 741	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$
62	61	adantr 471	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
63		simp-4r 782	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		simpllr 774	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65		opelxpi 4888	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
66	63, 64, 65	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67		vex 3060	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68		vex 3060	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
69	67, 68	op1std 6835	. . . . . . . . . . . . . . . . . . . . . . . . . 26
70	69	fveq2d 5896	. . . . . . . . . . . . . . . . . . . . . . . . 25
71	67, 68	op2ndd 6836	. . . . . . . . . . . . . . . . . . . . . . . . . 26
72	71	fveq2d 5896	. . . . . . . . . . . . . . . . . . . . . . . . 25
73	70, 72	oveq12d 6338	. . . . . . . . . . . . . . . . . . . . . . . 24
74		fveq2 5892	. . . . . . . . . . . . . . . . . . . . . . . . 25
75		df-ov 6323	. . . . . . . . . . . . . . . . . . . . . . . . 25
76	74, 75	syl6eqr 2514	. . . . . . . . . . . . . . . . . . . . . . . 24
77	73, 76	oveq12d 6338	. . . . . . . . . . . . . . . . . . . . . . 23
78	77	fvixp 7558	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
79	62, 66, 78	syl2anc 671	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	59, 79	syl5eqel 2544	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81		elmapi 7524	. . . . . . . . . . . . . . . . . . . 20
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	82	adantr 471	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84	83, 44	ffvelrnd 6051	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85		df-ov 6323	. . . . . . . . . . . . . . . . . . . . 21
86		opelxpi 4888	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
87	86	adantll 725	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
88		vex 3060	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
89	68, 88	op1std 6835	. . . . . . . . . . . . . . . . . . . . . . . . . 26
90	89	fveq2d 5896	. . . . . . . . . . . . . . . . . . . . . . . . 25
91	68, 88	op2ndd 6836	. . . . . . . . . . . . . . . . . . . . . . . . . 26
92	91	fveq2d 5896	. . . . . . . . . . . . . . . . . . . . . . . . 25
93	90, 92	oveq12d 6338	. . . . . . . . . . . . . . . . . . . . . . . 24
94		fveq2 5892	. . . . . . . . . . . . . . . . . . . . . . . . 25
95		df-ov 6323	. . . . . . . . . . . . . . . . . . . . . . . . 25
96	94, 95	syl6eqr 2514	. . . . . . . . . . . . . . . . . . . . . . . 24
97	93, 96	oveq12d 6338	. . . . . . . . . . . . . . . . . . . . . . 23
98	97	fvixp 7558	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
99	61, 87, 98	syl2anc 671	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
100	85, 99	syl5eqel 2544	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
101		elmapi 7524	. . . . . . . . . . . . . . . . . . . 20
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
103	102	adantr 471	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	103	ffvelrnda 6050	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105	48, 49, 50, 51, 52, 53, 56, 57, 58, 84, 104	comfeqval 15668	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
106	47, 105	eqeq12d 2477	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
107	106	ralbidva 2836	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
108	107	ralbidva 2836	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
109		eqid 2462	. . . . . . . . . . . . . . 15
110	24	ad2antrr 737	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
111		simpllr 774	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
112		simplr 767	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
113	35, 36, 109, 110, 111, 112	homfeqval 15657	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
114		simpr 467	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
115	35, 36, 109, 110, 112, 114	homfeqval 15657	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
116	115	raleqdv 3005	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
117	113, 116	raleqbidv 3013	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
118	108, 117	bitrd 261	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
119	118	ralbidva 2836	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ comp comp comp comp
120	119	ralbidva 2836	. . . . . . . . . 10 $/\$ $/\$ $/\$ comp comp comp comp
121	34, 120	anbi12d 722	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ comp comp $/\$ comp comp
122	121	ralbidva 2836	. . . . . . . 8 $/\$ $/\$ $/\$ comp comp $/\$ comp comp
123	23, 122	sylan2b 482	. . . . . . 7 $/\$ $/\$ $/\$ comp comp $/\$ comp comp
124	123	pm5.32da 651	. . . . . 6 $/\$ $/\$ $/\$ comp comp $/\$ $/\$ $/\$ comp comp
125		eqid 2462	. . . . . . . . . . . . . 14
126	8	ad2antrr 737	. . . . . . . . . . . . . 14 $/\$ $/\$ _f _f
127		simplr 767	. . . . . . . . . . . . . . 15 $/\$ $/\$
128		xp1st 6855	. . . . . . . . . . . . . . . 16
129	128	adantl 472	. . . . . . . . . . . . . . 15 $/\$ $/\$
130	127, 129	ffvelrnd 6051	. . . . . . . . . . . . . 14 $/\$ $/\$
131		xp2nd 6856	. . . . . . . . . . . . . . . 16
132	131	adantl 472	. . . . . . . . . . . . . . 15 $/\$ $/\$
133	127, 132	ffvelrnd 6051	. . . . . . . . . . . . . 14 $/\$ $/\$
134	48, 49, 125, 126, 130, 133	homfeqval 15657	. . . . . . . . . . . . 13 $/\$ $/\$
135	3	ad2antrr 737	. . . . . . . . . . . . . . . 16 $/\$ $/\$ _f _f
136	35, 36, 109, 135, 129, 132	homfeqval 15657	. . . . . . . . . . . . . . 15 $/\$ $/\$
137		df-ov 6323	. . . . . . . . . . . . . . 15
138		df-ov 6323	. . . . . . . . . . . . . . 15
139	136, 137, 138	3eqtr3g 2519	. . . . . . . . . . . . . 14 $/\$ $/\$
140		1st2nd2 6862	. . . . . . . . . . . . . . . 16
141	140	adantl 472	. . . . . . . . . . . . . . 15 $/\$ $/\$
142	141	fveq2d 5896	. . . . . . . . . . . . . 14 $/\$ $/\$
143	141	fveq2d 5896	. . . . . . . . . . . . . 14 $/\$ $/\$
144	139, 142, 143	3eqtr4d 2506	. . . . . . . . . . . . 13 $/\$ $/\$
145	134, 144	oveq12d 6338	. . . . . . . . . . . 12 $/\$ $/\$
146	145	ixpeq2dva 7568	. . . . . . . . . . 11 $/\$
147	3	homfeqbas 15656	. . . . . . . . . . . . . 14
148	147	sqxpeqd 4882	. . . . . . . . . . . . 13
149	148	adantr 471	. . . . . . . . . . . 12 $/\$
150	149	ixpeq1d 7565	. . . . . . . . . . 11 $/\$
151	146, 150	eqtrd 2496	. . . . . . . . . 10 $/\$
152	151	eleq2d 2525	. . . . . . . . 9 $/\$
153	152	pm5.32da 651	. . . . . . . 8 $/\$ $/\$
154	8	homfeqbas 15656	. . . . . . . . . 10
155	147, 154	feq23d 5750	. . . . . . . . 9
156	155	anbi1d 716	. . . . . . . 8 $/\$ $/\$
157	153, 156	bitrd 261	. . . . . . 7 $/\$ $/\$
158	147	adantr 471	. . . . . . . . . 10 $/\$
159	158	raleqdv 3005	. . . . . . . . . 10 $/\$ comp comp comp comp
160	158, 159	raleqbidv 3013	. . . . . . . . 9 $/\$ comp comp comp comp
161	160	anbi2d 715	. . . . . . . 8 $/\$ $/\$ comp comp $/\$ comp comp
162	147, 161	raleqbidva 3015	. . . . . . 7 $/\$ comp comp $/\$ comp comp
163	157, 162	anbi12d 722	. . . . . 6 $/\$ $/\$ $/\$ comp comp $/\$ $/\$ $/\$ comp comp
164	124, 163	bitrd 261	. . . . 5 $/\$ $/\$ $/\$