catpropd - Metamath Proof Explorer

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

Theorem catpropd 16369

Description: Two structures with the same base, hom-sets and composition operation are either both categories or neither. (Contributed by Mario Carneiro, 5-Jan-2017.)

**Hypotheses**
Ref	Expression
catpropd.1	_f _f
catpropd.2	comp_f comp_f
catpropd.3
catpropd.4

**Assertion**
Ref	Expression
catpropd

Proof of Theorem catpropd Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 473	. . . . . . . . 9 comp $/\$ comp comp comp comp comp
2	1	2ralimi 2953	. . . . . . . 8 comp $/\$ comp comp comp comp comp
3	2	2ralimi 2953	. . . . . . 7 comp $/\$ comp comp comp comp comp
4	3	adantl 482	. . . . . 6 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp
5	4	ralimi 2952	. . . . 5 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp
6	5	a1i 11	. . . 4 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp
7		simpl 473	. . . . . . . . 9 comp $/\$ comp comp comp comp comp
8	7	2ralimi 2953	. . . . . . . 8 comp $/\$ comp comp comp comp comp
9	8	2ralimi 2953	. . . . . . 7 comp $/\$ comp comp comp comp comp
10	9	adantl 482	. . . . . 6 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp
11	10	ralimi 2952	. . . . 5 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp
12	11	a1i 11	. . . 4 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp
13		nfra1 2941	. . . . . . . 8 comp
14		nfv 1843	. . . . . . . 8 comp
15		nfra1 2941	. . . . . . . . . 10 comp
16		nfv 1843	. . . . . . . . . 10 comp
17		nfra1 2941	. . . . . . . . . . . . . 14 comp
18		nfv 1843	. . . . . . . . . . . . . 14 comp
19		oveq1 6657	. . . . . . . . . . . . . . . . 17 comp comp
20	19	eleq1d 2686	. . . . . . . . . . . . . . . 16 comp comp
21	20	cbvralv 3171	. . . . . . . . . . . . . . 15 comp comp
22		oveq2 6658	. . . . . . . . . . . . . . . . 17 comp comp
23	22	eleq1d 2686	. . . . . . . . . . . . . . . 16 comp comp
24	23	ralbidv 2986	. . . . . . . . . . . . . . 15 comp comp
25	21, 24	syl5bb 272	. . . . . . . . . . . . . 14 comp comp
26	17, 18, 25	cbvral 3167	. . . . . . . . . . . . 13 comp comp
27		oveq2 6658	. . . . . . . . . . . . . . 15
28		oveq2 6658	. . . . . . . . . . . . . . . . 17 comp comp
29	28	oveqd 6667	. . . . . . . . . . . . . . . 16 comp comp
30		oveq2 6658	. . . . . . . . . . . . . . . 16
31	29, 30	eleq12d 2695	. . . . . . . . . . . . . . 15 comp comp
32	27, 31	raleqbidv 3152	. . . . . . . . . . . . . 14 comp comp
33	32	ralbidv 2986	. . . . . . . . . . . . 13 comp comp
34	26, 33	syl5bb 272	. . . . . . . . . . . 12 comp comp
35	34	cbvralv 3171	. . . . . . . . . . 11 comp comp
36		oveq2 6658	. . . . . . . . . . . . 13
37		oveq1 6657	. . . . . . . . . . . . . 14
38		opeq2 4403	. . . . . . . . . . . . . . . . 17
39	38	oveq1d 6665	. . . . . . . . . . . . . . . 16 comp comp
40	39	oveqd 6667	. . . . . . . . . . . . . . 15 comp comp
41	40	eleq1d 2686	. . . . . . . . . . . . . 14 comp comp
42	37, 41	raleqbidv 3152	. . . . . . . . . . . . 13 comp comp
43	36, 42	raleqbidv 3152	. . . . . . . . . . . 12 comp comp
44	43	ralbidv 2986	. . . . . . . . . . 11 comp comp
45	35, 44	syl5bb 272	. . . . . . . . . 10 comp comp
46	15, 16, 45	cbvral 3167	. . . . . . . . 9 comp comp
47		oveq1 6657	. . . . . . . . . . . . 13
48		opeq1 4402	. . . . . . . . . . . . . . . . 17
49	48	oveq1d 6665	. . . . . . . . . . . . . . . 16 comp comp
50	49	oveqd 6667	. . . . . . . . . . . . . . 15 comp comp
51		oveq1 6657	. . . . . . . . . . . . . . 15
52	50, 51	eleq12d 2695	. . . . . . . . . . . . . 14 comp comp
53	52	ralbidv 2986	. . . . . . . . . . . . 13 comp comp
54	47, 53	raleqbidv 3152	. . . . . . . . . . . 12 comp comp
55	54	ralbidv 2986	. . . . . . . . . . 11 comp comp
56		ralcom 3098	. . . . . . . . . . 11 comp comp
57	55, 56	syl6bb 276	. . . . . . . . . 10 comp comp
58	57	ralbidv 2986	. . . . . . . . 9 comp comp
59	46, 58	syl5bb 272	. . . . . . . 8 comp comp
60	13, 14, 59	cbvral 3167	. . . . . . 7 comp comp
61	60	biimpi 206	. . . . . 6 comp comp
62	61	ancri 575	. . . . 5 comp comp $/\$ comp
63		r19.26 3064	. . . . . . . . . . . 12 comp $/\$ comp comp $/\$ comp
64		r19.26 3064	. . . . . . . . . . . . . . 15 comp $/\$ comp comp $/\$ comp
65		r19.26 3064	. . . . . . . . . . . . . . . . . . . . . . . 24 comp $/\$ comp comp $/\$ comp
66		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
67		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
68		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp
69		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 comp comp
70		catpropd.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 _f _f
71	70	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ _f _f
72	71	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
73	72	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ $/\$ comp _f _f
74		catpropd.2	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 comp_f comp_f
75	74	ad5antr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ comp_f comp_f
76	75	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ $/\$ comp comp_f comp_f
77		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$
78	77	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$
79	78	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ $/\$ comp
80		simp-4r 807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$
81	80	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ $/\$ comp
82		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ $/\$ comp
83		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$
84	83	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ $/\$ comp
85		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ $/\$ comp comp
86	66, 67, 68, 69, 73, 76, 79, 81, 82, 84, 85	comfeqval 16368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ $/\$ comp comp comp comp comp
87		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$
88	87	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ $/\$ comp
89		simp-4r 807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ $/\$ comp comp
90		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ $/\$ comp
91	66, 67, 68, 69, 73, 76, 79, 88, 82, 89, 90	comfeqval 16368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ $/\$ comp comp comp comp comp
92	86, 91	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ $/\$ comp comp comp comp comp comp comp comp comp
93	92	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ $/\$ comp comp comp comp comp comp comp comp comp
94	93	ralimdva 2962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ comp comp comp comp comp comp comp comp comp
95		ralbi 3068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp
96	94, 95	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ comp comp comp comp comp comp comp comp comp
97	96	ralimdva 2962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp comp comp comp comp comp comp
98	97	impancom 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp comp comp comp comp comp comp
99	98	impr 649	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ comp comp comp comp comp comp comp comp comp
100		ralbi 3068	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp comp
101	99, 100	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ comp comp comp comp comp comp comp comp comp
102	101	anbi2d 740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
103	102	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
104	103	ralimdva 2962	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ comp $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
105	65, 104	syl5bir 233	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ comp $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
106	105	expdimp 453	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
107		ralbi 3068	. . . . . . . . . . . . . . . . . . . . . 22 comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
108	106, 107	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
109	108	an32s 846	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ comp $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
110	109	ralimdva 2962	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ comp comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
111		ralbi 3068	. . . . . . . . . . . . . . . . . . 19 comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
112	110, 111	syl6 35	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ comp comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
113	112	expimpd 629	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ comp $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
114	113	ralimdva 2962	. . . . . . . . . . . . . . . 16 $/\$ $/\$ comp $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
115		ralbi 3068	. . . . . . . . . . . . . . . 16 comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
116	114, 115	syl6 35	. . . . . . . . . . . . . . 15 $/\$ $/\$ comp $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
117	64, 116	syl5bir 233	. . . . . . . . . . . . . 14 $/\$ $/\$ comp $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
118	117	ralimdva 2962	. . . . . . . . . . . . 13 $/\$ comp $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
119		ralbi 3068	. . . . . . . . . . . . 13 comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
120	118, 119	syl6 35	. . . . . . . . . . . 12 $/\$ comp $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
121	63, 120	syl5bir 233	. . . . . . . . . . 11 $/\$ comp $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
122	121	imp 445	. . . . . . . . . 10 $/\$ $/\$ comp $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
123	122	an4s 869	. . . . . . . . 9 $/\$ comp $/\$ $/\$ comp comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
124	123	anbi2d 740	. . . . . . . 8 $/\$ comp $/\$ $/\$ comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
125	124	expr 643	. . . . . . 7 $/\$ comp $/\$ comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
126	125	ralimdva 2962	. . . . . 6 $/\$ comp comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
127	126	expimpd 629	. . . . 5 comp $/\$ comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
128		ralbi 3068	. . . . 5 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
129	62, 127, 128	syl56 36	. . . 4 comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
130	6, 12, 129	pm5.21ndd 369	. . 3 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
131	70	homfeqbas 16356	. . . 4
132		eqid 2622	. . . . . . 7
133		simpr 477	. . . . . . 7 $/\$
134	66, 67, 132, 71, 133, 133	homfeqval 16357	. . . . . 6 $/\$
135	131	ad2antrr 762	. . . . . . 7 $/\$ $/\$
136	71	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$ $/\$ _f _f
137		simpr 477	. . . . . . . . . 10 $/\$ $/\$ $/\$
138		simpllr 799	. . . . . . . . . 10 $/\$ $/\$ $/\$
139	66, 67, 132, 136, 137, 138	homfeqval 16357	. . . . . . . . 9 $/\$ $/\$ $/\$
140	70	ad4antr 768	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ _f _f
141	74	ad4antr 768	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ comp_f comp_f
142		simplr 792	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
143		simp-4r 807	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
144		simpr 477	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
145		simpllr 799	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
146	66, 67, 68, 69, 140, 141, 142, 143, 143, 144, 145	comfeqval 16368	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ comp comp
147	146	eqeq1d 2624	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ comp comp
148	139, 147	raleqbidva 3154	. . . . . . . 8 $/\$ $/\$ $/\$ comp comp
149	66, 67, 132, 136, 138, 137	homfeqval 16357	. . . . . . . . 9 $/\$ $/\$ $/\$
150	70	ad4antr 768	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ _f _f
151	74	ad4antr 768	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ comp_f comp_f
152		simp-4r 807	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
153		simplr 792	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
154		simpllr 799	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
155		simpr 477	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
156	66, 67, 68, 69, 150, 151, 152, 152, 153, 154, 155	comfeqval 16368	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ comp comp
157	156	eqeq1d 2624	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ comp comp
158	149, 157	raleqbidva 3154	. . . . . . . 8 $/\$ $/\$ $/\$ comp comp
159	148, 158	anbi12d 747	. . . . . . 7 $/\$ $/\$ $/\$ comp $/\$ comp comp $/\$ comp
160	135, 159	raleqbidva 3154	. . . . . 6 $/\$ $/\$ comp $/\$ comp comp $/\$ comp
161	134, 160	rexeqbidva 3155	. . . . 5 $/\$ comp $/\$ comp comp $/\$ comp
162	131	adantr 481	. . . . . 6 $/\$
163	162	adantr 481	. . . . . . 7 $/\$ $/\$
164	71	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ _f _f
165		simplr 792	. . . . . . . . 9 $/\$ $/\$ $/\$
166	66, 67, 132, 164, 77, 165	homfeqval 16357	. . . . . . . 8 $/\$ $/\$ $/\$
167		simpr 477	. . . . . . . . . . 11 $/\$ $/\$ $/\$
168	66, 67, 132, 164, 165, 167	homfeqval 16357	. . . . . . . . . 10 $/\$ $/\$ $/\$
169	168	adantr 481	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
170		simpr 477	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
171	66, 67, 68, 69, 72, 75, 78, 80, 87, 83, 170	comfeqval 16368	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
172	66, 67, 132, 164, 77, 167	homfeqval 16357	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
173	172	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
174	171, 173	eleq12d 2695	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
175	162	ad4antr 768	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
176	72	adantr 481	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
177		simp-4r 807	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178		simpr 477	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
179	66, 67, 132, 176, 177, 178	homfeqval 16357	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
180	164	ad4antr 768	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ _f _f
181	74	ad7antr 774	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp_f comp_f
182	165	ad4antr 768	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
183	167	ad4antr 768	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
184		simplr 792	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
185		simpllr 799	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
186		simpr 477	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
187	66, 67, 68, 69, 180, 181, 182, 183, 184, 185, 186	comfeqval 16368	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
188	187	oveq1d 6665	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
189	77	ad4antr 768	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
190		simp-4r 807	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
191	66, 67, 68, 69, 180, 181, 189, 182, 183, 190, 185	comfeqval 16368	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp
192	191	oveq2d 6666	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp
193	188, 192	eqeq12d 2637	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp comp comp comp comp
194	179, 193	raleqbidva 3154	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp comp comp comp comp
195	175, 194	raleqbidva 3154	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ comp comp comp comp comp comp comp comp
196	174, 195	anbi12d 747	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
197	169, 196	raleqbidva 3154	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
198	166, 197	raleqbidva 3154	. . . . . . 7 $/\$ $/\$ $/\$ comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
199	163, 198	raleqbidva 3154	. . . . . 6 $/\$ $/\$ comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
200	162, 199	raleqbidva 3154	. . . . 5 $/\$ comp $/\$ comp comp comp comp comp $/\$ comp comp comp comp
201	161, 200	anbi12d 747	. . . 4 $/\$ comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
202	131, 201	raleqbidva 3154	. . 3 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
203	130, 202	bitrd 268	. 2 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
204		catpropd.3	. . 3
205	66, 67, 68	iscat 16333	. . 3 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
206	204, 205	syl 17	. 2 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
207		catpropd.4	. . 3
208		eqid 2622	. . . 4
209	208, 132, 69	iscat 16333	. . 3 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
210	207, 209	syl 17	. 2 comp $/\$ comp $/\$ comp $/\$ comp comp comp comp
211	203, 206, 210	3bitr4d 300	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $/\$ wa 384

wceq 1483

wcel 1990

wral 2912

wrex 2913

cop 4183

cfv 5888 (class class class)co 6650

cbs 15857

chom 15952 compcco 15953

ccat 16325

_f chomf 16327 comp_fccomf 16328

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-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-ov 6653 df-oprab 6654 df-mpt2 6655 df-1st 7168 df-2nd 7169 df-cat 16329 df-homf 16331 df-comf 16332

This theorem is referenced by: cidpropd 16370 resscat 16512 funcpropd 16560

W3C validator