isfuna - Mathbox for Frédéric Liné

Table of Contents

Mathbox for Frédéric Liné

< Previous Next >
Related theorems
Unicode version

Theorem isfuna 15182

Description: The class of functors between the categories

and

**Hypotheses**
Ref	Expression
isfuna.1	O₁ id
isfuna.2	M₁ dom
isfuna.3	D₁ dom
isfuna.4	C₁ cod
isfuna.5	I₁ id
isfuna.6	Ro₁ o
isfuna.7	O₂ id
isfuna.8	M₂ dom
isfuna.9	D₂ dom
isfuna.10	C₂ cod
isfuna.11	I₂ id
isfuna.12	Ro₂ o

**Assertion**
Ref	Expression
isfuna	Cat $/\$ Cat Func M₁M₂ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂

Distinct variable groups:

,M₁,

,M₂

,O₁

,O₂

**Proof of Theorem isfuna**
Step	Hyp	Ref	Expression
1		isfuna.8	. . . . . . . . 9 M₂ dom
2		fvex 4689	. . . . . . . . . 10 dom
3	2	dmex 4208	. . . . . . . . 9 dom
4	1, 3	eqeltri 1967	. . . . . . . 8 M₂
5		isfuna.2	. . . . . . . . 9 M₁ dom
6		fvex 4689	. . . . . . . . . 10 dom
7	6	dmex 4208	. . . . . . . . 9 dom
8	5, 7	eqeltri 1967	. . . . . . . 8 M₁
9	4, 8	pm3.2i 307	. . . . . . 7 M₂ $/\$ M₁
10	9	a1i 8	. . . . . 6 Cat $/\$ Cat M₂ $/\$ M₁
11		elmapg 5392	. . . . . 6 M₂ $/\$ M₁ M₂ M₁ M₁M₂
12	10, 11	syl 12	. . . . 5 Cat $/\$ Cat M₂ M₁ M₁M₂
13	12	anbi1d 679	. . . 4 Cat $/\$ Cat M₂ M₁ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂ M₁M₂ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂
14	13	abbidv 2008	. . 3 Cat $/\$ Cat M₂ M₁ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂ M₁M₂ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂
15	9	a1i 8	. . . . . . . 8 Cat $/\$ Cat M₂ $/\$ M₁
16		mapvalg 5389	. . . . . . . 8 M₂ $/\$ M₁ M₂ M₁ M₁M₂
17	15, 16	syl 12	. . . . . . 7 Cat $/\$ Cat M₂ M₁ M₁M₂
18	17	ancoms 484	. . . . . 6 Cat $/\$ Cat M₂ M₁ M₁M₂
19	8, 4	pm3.2i 307	. . . . . . . 8 M₁ $/\$ M₂
20	19	a1i 8	. . . . . . 7 Cat $/\$ Cat M₁ $/\$ M₂
21		mapex 5387	. . . . . . 7 M₁ $/\$ M₂ M₁M₂
22	20, 21	syl 12	. . . . . 6 Cat $/\$ Cat M₁M₂
23	18, 22	eqeltrd 1971	. . . . 5 Cat $/\$ Cat M₂ M₁
24		rabexg 3460	. . . . 5 M₂ M₁ M₂ M₁ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂
25	23, 24	syl 12	. . . 4 Cat $/\$ Cat M₂ M₁ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂
26		df-rab 2112	. . . 4 M₂ M₁ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂ M₂ M₁ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂
27	25, 26	syl5eqelr 1976	. . 3 Cat $/\$ Cat M₂ M₁ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂
28	14, 27	eqeltrrd 1972	. 2 Cat $/\$ Cat M₁M₂ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂
29		fveq2 4681	. . . . . . . . 9 dom dom
30	29	dmeqd 4159	. . . . . . . 8 dom dom
31	30, 5	syl6eqr 1946	. . . . . . 7 dom M₁
32	31	feq2d 4557	. . . . . 6 dom dom M₁ dom
33		fveq2 4681	. . . . . . . . 9 id id
34	33	dmeqd 4159	. . . . . . . 8 id id
35	33	fveq1d 4683	. . . . . . . . . . 11 id id
36	35	fveq2d 4685	. . . . . . . . . 10 id id
37	36	eqeq1d 1892	. . . . . . . . 9 id id id id
38	37	rexbidv 2124	. . . . . . . 8 idid id idid id
39	34, 38	raleqbidv 2274	. . . . . . 7 id idid id id idid id
40	29	fveq1d 4683	. . . . . . . . . . . 12 dom dom
41	33, 40	fveq12d 10152	. . . . . . . . . . 11 iddom iddom
42	41	fveq2d 4685	. . . . . . . . . 10 iddom iddom
43	42	eqeq1d 1892	. . . . . . . . 9 iddom iddom iddom iddom
44	30, 43	raleqbidv 2274	. . . . . . . 8 domiddom iddom domiddom iddom
45		fveq2 4681	. . . . . . . . . . . . 13 cod cod
46	45	fveq1d 4683	. . . . . . . . . . . 12 cod cod
47	33, 46	fveq12d 10152	. . . . . . . . . . 11 idcod idcod
48	47	fveq2d 4685	. . . . . . . . . 10 idcod idcod
49	48	eqeq1d 1892	. . . . . . . . 9 idcod idcod idcod idcod
50	30, 49	raleqbidv 2274	. . . . . . . 8 domidcod idcod domidcod idcod
51	44, 50	anbi12d 690	. . . . . . 7 domiddom iddom $/\$ domidcod idcod domiddom iddom $/\$ domidcod idcod
52	45	fveq1d 4683	. . . . . . . . . . 11 cod cod
53	52, 40	eqeq12d 1899	. . . . . . . . . 10 cod dom cod dom
54		fveq2 4681	. . . . . . . . . . . . 13 o o
55	54	opreqd 4899	. . . . . . . . . . . 12 o o
56	55	fveq2d 4685	. . . . . . . . . . 11 o o
57	56	eqeq1d 1892	. . . . . . . . . 10 o o o o
58	53, 57	imbi12d 688	. . . . . . . . 9 cod dom o o cod dom o o
59	30, 58	raleqbidv 2274	. . . . . . . 8 domcod dom o o domcod dom o o
60	30, 59	raleqbidv 2274	. . . . . . 7 dom domcod dom o o dom domcod dom o o
61	39, 51, 60	3anbi123d 1168	. . . . . 6 id idid id $/\$ domiddom iddom $/\$ domidcod idcod $/\$ dom domcod dom o o id idid id $/\$ domiddom iddom $/\$ domidcod idcod $/\$ dom domcod dom o o
62	32, 61	anbi12d 690	. . . . 5 dom dom $/\$ id idid id $/\$ domiddom iddom $/\$ domidcod idcod $/\$ dom domcod dom o o M₁ dom $/\$ id idid id $/\$ domiddom iddom $/\$ domidcod idcod $/\$ dom domcod dom o o
63	62	abbidv 2008	. . . 4 dom dom $/\$ id idid id $/\$ domiddom iddom $/\$ domidcod idcod $/\$ dom domcod dom o o M₁ dom $/\$ id idid id $/\$ domiddom iddom $/\$ domidcod idcod $/\$ dom domcod dom o o
64		fveq2 4681	. . . . . . . . 9 dom dom
65	64	dmeqd 4159	. . . . . . . 8 dom dom
66	65, 1	syl6eqr 1946	. . . . . . 7 dom M₂
67		feq3 4553	. . . . . . 7 dom M₂ M₁ dom M₁M₂
68	66, 67	syl 12	. . . . . 6 M₁ dom M₁M₂
69		isfuna.1	. . . . . . . . . 10 O₁ id
70	69	a1i 8	. . . . . . . . 9 O₁ id
71	70	eqcomd 1889	. . . . . . . 8 id O₁
72		fveq2 4681	. . . . . . . . . . 11 id id
73	72	dmeqd 4159	. . . . . . . . . 10 id id
74		isfuna.7	. . . . . . . . . 10 O₂ id
75	73, 74	syl6eqr 1946	. . . . . . . . 9 id O₂
76		isfuna.5	. . . . . . . . . . . . . 14 I₁ id
77	76	a1i 8	. . . . . . . . . . . . 13 I₁ id
78	77	eqcomd 1889	. . . . . . . . . . . 12 id I₁
79	78	fveq1d 4683	. . . . . . . . . . 11 id I₁
80	79	fveq2d 4685	. . . . . . . . . 10 id I₁
81		isfuna.11	. . . . . . . . . . . 12 I₂ id
82	72, 81	syl6eqr 1946	. . . . . . . . . . 11 id I₂
83	82	fveq1d 4683	. . . . . . . . . 10 id I₂
84	80, 83	eqeq12d 1899	. . . . . . . . 9 id id I₁ I₂
85	75, 84	rexeqbidv 2275	. . . . . . . 8 idid id O₂ I₁ I₂
86	71, 85	raleqbidv 2274	. . . . . . 7 id idid id O₁ O₂ I₁ I₂
87	5	a1i 8	. . . . . . . . . 10 M₁ dom
88	87	eqcomd 1889	. . . . . . . . 9 dom M₁
89		isfuna.3	. . . . . . . . . . . . . . 15 D₁ dom
90	89	a1i 8	. . . . . . . . . . . . . 14 D₁ dom
91	90	fveq1d 4683	. . . . . . . . . . . . 13 D₁ dom
92	91	eqcomd 1889	. . . . . . . . . . . 12 dom D₁
93	78, 92	fveq12d 10152	. . . . . . . . . . 11 iddom I₁D₁
94	93	fveq2d 4685	. . . . . . . . . 10 iddom I₁D₁
95	72	fveq1d 4683	. . . . . . . . . . 11 iddom iddom
96	64	fveq1d 4683	. . . . . . . . . . . 12 dom dom
97	96	fveq2d 4685	. . . . . . . . . . 11 iddom iddom
98	81	a1i 8	. . . . . . . . . . . . 13 I₂ id
99	98	eqcomd 1889	. . . . . . . . . . . 12 id I₂
100		isfuna.9	. . . . . . . . . . . . . . 15 D₂ dom
101	100	a1i 8	. . . . . . . . . . . . . 14 D₂ dom
102	101	eqcomd 1889	. . . . . . . . . . . . 13 dom D₂
103	102	fveq1d 4683	. . . . . . . . . . . 12 dom D₂
104	99, 103	fveq12d 10152	. . . . . . . . . . 11 iddom I₂D₂
105	95, 97, 104	3eqtrd 1929	. . . . . . . . . 10 iddom I₂D₂
106	94, 105	eqeq12d 1899	. . . . . . . . 9 iddom iddom I₁D₁ I₂D₂
107	88, 106	raleqbidv 2274	. . . . . . . 8 domiddom iddom M₁ I₁D₁ I₂D₂
108	87	eleq2d 1964	. . . . . . . . . . 11 M₁ dom
109	108	bicomd 580	. . . . . . . . . 10 dom M₁
110		isfuna.4	. . . . . . . . . . . . . . . 16 C₁ cod
111	110	a1i 8	. . . . . . . . . . . . . . 15 C₁ cod
112	111	eqcomd 1889	. . . . . . . . . . . . . 14 cod C₁
113	112	fveq1d 4683	. . . . . . . . . . . . 13 cod C₁
114	78, 113	fveq12d 10152	. . . . . . . . . . . 12 idcod I₁C₁
115	114	fveq2d 4685	. . . . . . . . . . 11 idcod I₁C₁
116		fveq2 4681	. . . . . . . . . . . . . 14 cod cod
117		isfuna.10	. . . . . . . . . . . . . 14 C₂ cod
118	116, 117	syl6eqr 1946	. . . . . . . . . . . . 13 cod C₂
119	118	fveq1d 4683	. . . . . . . . . . . 12 cod C₂
120	82, 119	fveq12d 10152	. . . . . . . . . . 11 idcod I₂C₂
121	115, 120	eqeq12d 1899	. . . . . . . . . 10 idcod idcod I₁C₁ I₂C₂
122	109, 121	imbi12d 688	. . . . . . . . 9 dom idcod idcod M₁ I₁C₁ I₂C₂
123	122	ralbidv2 2125	. . . . . . . 8 domidcod idcod M₁ I₁C₁ I₂C₂
124	107, 123	anbi12d 690	. . . . . . 7 domiddom iddom $/\$ domidcod idcod M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂
125	5	eleq2i 1961	. . . . . . . . . . 11 M₁ dom
126	125	a1i 8	. . . . . . . . . 10 M₁ dom
127	126	bicomd 580	. . . . . . . . 9 dom M₁
128	87	eleq2d 1964	. . . . . . . . . . . 12 M₁ dom
129	128	bicomd 580	. . . . . . . . . . 11 dom M₁
130	111	fveq1d 4683	. . . . . . . . . . . . . 14 C₁ cod
131	130	eqcomd 1889	. . . . . . . . . . . . 13 cod C₁
132	131, 92	eqeq12d 1899	. . . . . . . . . . . 12 cod dom C₁ D₁
133		isfuna.6	. . . . . . . . . . . . . . . . 17 Ro₁ o
134	133	a1i 8	. . . . . . . . . . . . . . . 16 Ro₁ o
135	134	eqcomd 1889	. . . . . . . . . . . . . . 15 o Ro₁
136	135	opreqd 4899	. . . . . . . . . . . . . 14 o Ro₁
137	136	fveq2d 4685	. . . . . . . . . . . . 13 o Ro₁
138		fveq2 4681	. . . . . . . . . . . . . . 15 o o
139		isfuna.12	. . . . . . . . . . . . . . 15 Ro₂ o
140	138, 139	syl6eqr 1946	. . . . . . . . . . . . . 14 o Ro₂
141	140	opreqd 4899	. . . . . . . . . . . . 13 o Ro₂
142	137, 141	eqeq12d 1899	. . . . . . . . . . . 12 o o Ro₁ Ro₂
143	132, 142	imbi12d 688	. . . . . . . . . . 11 cod dom o o C₁ D₁ Ro₁ Ro₂
144	129, 143	imbi12d 688	. . . . . . . . . 10 dom cod dom o o M₁ C₁ D₁ Ro₁ Ro₂
145	144	ralbidv2 2125	. . . . . . . . 9 domcod dom o o M₁ C₁ D₁ Ro₁ Ro₂
146	127, 145	imbi12d 688	. . . . . . . 8 dom domcod dom o o M₁ M₁ C₁ D₁ Ro₁ Ro₂
147	146	ralbidv2 2125	. . . . . . 7 dom domcod dom o o M₁ M₁ C₁ D₁ Ro₁ Ro₂
148	86, 124, 147	3anbi123d 1168	. . . . . 6 id idid id $/\$ domiddom iddom $/\$ domidcod idcod $/\$ dom domcod dom o o O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂
149	68, 148	anbi12d 690	. . . . 5 M₁ dom $/\$ id idid id $/\$ domiddom iddom $/\$ domidcod idcod $/\$ dom domcod dom o o M₁M₂ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂
150	149	abbidv 2008	. . . 4 M₁ dom $/\$ id idid id $/\$ domiddom iddom $/\$ domidcod idcod $/\$ dom domcod dom o o M₁M₂ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂
151		df-func 15181	. . . 4 Func Cat $/\$ Cat $/\$ dom dom $/\$ id idid id $/\$ domiddom iddom $/\$ domidcod idcod $/\$ dom domcod dom o o
152	63, 150, 151	oprabval2g 4956	. . 3 Cat $/\$ Cat $/\$ M₁M₂ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂ Func M₁M₂ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂
153		df-opr 4886	. . 3 Func Func
154	152, 153	syl5eqr 1942	. 2 Cat $/\$ Cat $/\$ M₁M₂ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂ Func M₁M₂ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂
155	28, 154	mpd3an3 1192	1 Cat $/\$ Cat Func M₁M₂ $/\$ O₁ O₂ I₁ I₂ $/\$ M₁ I₁D₁ I₂D₂ $/\$ M₁ I₁C₁ I₂C₂ $/\$ M₁ M₁ C₁ D₁ Ro₁ Ro₂

Colors of variables: wff set class

Syntax hints:

wi 3

wb 163 $/\$ wa 240 $/\$ w3a 858

wceq 1298

wcel 1300

cab 1871

wral 2105

wrex 2106

crab 2108

cvv 2292

cop 3046

cdm 3986

wf 3994

cfv 3998 (class class class)co 4884

cmap 5381 domcdom_ 15059 codccod_ 15060 idcid_ 15061 oco_ 15062 Cat ccat 15099 Func cfunc 15179

This theorem is referenced by: isfunb 15183

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-nul 2876 df-pw 3035 df-sn 3049 df-pr 3050 df-op 3053 df-uni 3178 df-br 3339 df-opab 3396 df-id 3586 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-fv 4014 df-opr 4886 df-oprab 4887 df-map 5383 df-func 15181