idfisf - Mathbox for Frédéric Liné

Mathbox for Frédéric Liné

< Previous Next >
Related theorems
Unicode version

Theorem idfisf 15189

Description: The identity functor is a functor.

**Assertion**
Ref	Expression
idfisf	Cat dom Func

**Proof of Theorem idfisf**
Step	Hyp	Ref	Expression
1		fvex 4689	. . . . 5 dom
2	1	dmex 4208	. . . 4 dom
3		resiexg 4253	. . . 4 dom dom
4	2, 3	ax-mp 7	. . 3 dom
5		eqid 1884	. . . . . . . . . . . . 13 dom dom
6		eqid 1884	. . . . . . . . . . . . 13 id id
7		eqid 1884	. . . . . . . . . . . . 13 id id
8	5, 6, 7	jdmo 15125	. . . . . . . . . . . 12 Cat $/\$ id id dom
9		fvresi 4819	. . . . . . . . . . . 12 id dom domid id
10	8, 9	syl 12	. . . . . . . . . . 11 Cat $/\$ id domid id
11		fveq2 4681	. . . . . . . . . . . . . . 15 id id
12	11	eqeq2d 1895	. . . . . . . . . . . . . 14 domid id domid id
13	12	rcla4ev 2381	. . . . . . . . . . . . 13 id $/\$ domid id id domid id
14	13	ex 402	. . . . . . . . . . . 12 id domid id id domid id
15	14	adantl 424	. . . . . . . . . . 11 Cat $/\$ id domid id id domid id
16	10, 15	mpd 29	. . . . . . . . . 10 Cat $/\$ id id domid id
17	16	ex 402	. . . . . . . . 9 Cat id id domid id
18	17	r19.21aiv 2175	. . . . . . . 8 Cat id id domid id
19		simpl 346	. . . . . . . . . . . . . 14 Cat $/\$ dom Cat
20		eqid 1884	. . . . . . . . . . . . . . 15 dom dom
21	5, 6, 20	dmo 15123	. . . . . . . . . . . . . 14 Cat $/\$ dom dom id
22	19, 21	jca 310	. . . . . . . . . . . . 13 Cat $/\$ dom Cat $/\$ dom id
23	5, 6, 7	jdmo 15125	. . . . . . . . . . . . 13 Cat $/\$ dom id iddom dom
24		fvresi 4819	. . . . . . . . . . . . 13 iddom dom domiddom iddom
25	22, 23, 24	3syl 24	. . . . . . . . . . . 12 Cat $/\$ dom domiddom iddom
26		fvresi 4819	. . . . . . . . . . . . . . . 16 dom dom
27	26	eqcomd 1889	. . . . . . . . . . . . . . 15 dom dom
28	27	fveq2d 4685	. . . . . . . . . . . . . 14 dom dom dom dom
29	28	fveq2d 4685	. . . . . . . . . . . . 13 dom iddom iddom dom
30	29	adantl 424	. . . . . . . . . . . 12 Cat $/\$ dom iddom iddom dom
31	25, 30	eqtrd 1925	. . . . . . . . . . 11 Cat $/\$ dom domiddom iddom dom
32	31	ex 402	. . . . . . . . . 10 Cat dom domiddom iddom dom
33	32	r19.21aiv 2175	. . . . . . . . 9 Cat dom domiddom iddom dom
34		eqid 1884	. . . . . . . . . . . . . . 15 cod cod
35	5, 6, 34	cdmo 15124	. . . . . . . . . . . . . 14 Cat $/\$ dom cod id
36	19, 35	jca 310	. . . . . . . . . . . . 13 Cat $/\$ dom Cat $/\$ cod id
37	5, 6, 7	jdmo 15125	. . . . . . . . . . . . 13 Cat $/\$ cod id idcod dom
38		fvresi 4819	. . . . . . . . . . . . 13 idcod dom domidcod idcod
39	36, 37, 38	3syl 24	. . . . . . . . . . . 12 Cat $/\$ dom domidcod idcod
40	27	fveq2d 4685	. . . . . . . . . . . . . 14 dom cod cod dom
41	40	fveq2d 4685	. . . . . . . . . . . . 13 dom idcod idcod dom
42	41	adantl 424	. . . . . . . . . . . 12 Cat $/\$ dom idcod idcod dom
43	39, 42	eqtrd 1925	. . . . . . . . . . 11 Cat $/\$ dom domidcod idcod dom
44	43	ex 402	. . . . . . . . . 10 Cat dom domidcod idcod dom
45	44	r19.21aiv 2175	. . . . . . . . 9 Cat dom domidcod idcod dom
46	33, 45	jca 310	. . . . . . . 8 Cat dom domiddom iddom dom $/\$ dom domidcod idcod dom
47		eqid 1884	. . . . . . . . . . . . . . . 16 o o
48	5, 20, 34, 47	cmpmorp 15126	. . . . . . . . . . . . . . 15 Cat $/\$ dom $/\$ dom dom cod o dom
49	48	com12 14	. . . . . . . . . . . . . 14 dom cod Cat $/\$ dom $/\$ dom o dom
50	49	eqcoms 1887	. . . . . . . . . . . . 13 cod dom Cat $/\$ dom $/\$ dom o dom
51	50	com12 14	. . . . . . . . . . . 12 Cat $/\$ dom $/\$ dom cod dom o dom
52		fvresi 4819	. . . . . . . . . . . . . . 15 o dom domo o
53		fvresi 4819	. . . . . . . . . . . . . . . . 17 dom dom
54	26, 53	opreqan12rd 4903	. . . . . . . . . . . . . . . 16 dom $/\$ dom domo dom o
55	54	eqcomd 1889	. . . . . . . . . . . . . . 15 dom $/\$ dom o domo dom
56	52, 55	sylan9eqr 1951	. . . . . . . . . . . . . 14 dom $/\$ dom $/\$ o dom domo domo dom
57	56	ex 402	. . . . . . . . . . . . 13 dom $/\$ dom o dom domo domo dom
58	57	3adant1 894	. . . . . . . . . . . 12 Cat $/\$ dom $/\$ dom o dom domo domo dom
59	51, 58	syld 30	. . . . . . . . . . 11 Cat $/\$ dom $/\$ dom cod dom domo domo dom
60	59	3com23 1074	. . . . . . . . . 10 Cat $/\$ dom $/\$ dom cod dom domo domo dom
61	60	3expib 1070	. . . . . . . . 9 Cat dom $/\$ dom cod dom domo domo dom
62	61	r19.21aivv 2183	. . . . . . . 8 Cat dom domcod dom domo domo dom
63	18, 46, 62	3jca 1050	. . . . . . 7 Cat id id domid id $/\$ dom domiddom iddom dom $/\$ dom domidcod idcod dom $/\$ dom domcod dom domo domo dom
64		f1oi 4671	. . . . . . . 8 dom dom dom
65		f1of 4635	. . . . . . . 8 dom dom dom dom dom dom
66	64, 65	ax-mp 7	. . . . . . 7 dom dom dom
67	63, 66	jctil 316	. . . . . 6 Cat dom dom dom $/\$ id id domid id $/\$ dom domiddom iddom dom $/\$ dom domidcod idcod dom $/\$ dom domcod dom domo domo dom
68	67	3ad2ant1 897	. . . . 5 Cat $/\$ Cat $/\$ dom dom dom dom $/\$ id id domid id $/\$ dom domiddom iddom dom $/\$ dom domidcod idcod dom $/\$ dom domcod dom domo domo dom
69	6, 5, 20, 34, 7, 47, 6, 5, 20, 34, 7, 47	isfunb 15183	. . . . 5 Cat $/\$ Cat $/\$ dom dom Func dom dom dom $/\$ id id domid id $/\$ dom domiddom iddom dom $/\$ dom domidcod idcod dom $/\$ dom domcod dom domo domo dom
70	68, 69	mpbird 213	. . . 4 Cat $/\$ Cat $/\$ dom dom Func
71	70	3exp 1066	. . 3 Cat Cat dom dom Func
72	4, 71	mpii 56	. 2 Cat Cat dom Func
73	72	pm2.43i 78	1 Cat dom Func

Colors of variables: wff set class

Syntax hints:

wi 3 $/\$ wa 240 $/\$ w3a 858

wceq 1298

wcel 1300

wral 2105

wrex 2106

cvv 2292

cop 3046

cid 3582

cdm 3986

cres 3988

wf 3994

wf1o 3997

cfv 3998 (class class class)co 4884 domcdom_ 15059 codccod_ 15060 idcid_ 15061 oco_ 15062 Cat ccat 15099 Func cfunc 15179

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-int 3215 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-f1 4011 df-fo 4012 df-f1o 4013 df-fv 4014 df-opr 4886 df-oprab 4887 df-1st 5020 df-2nd 5021 df-map 5383 df-alg 15063 df-doma 15064 df-coda 15065 df-ida 15066 df-cmpa 15067 df-ded 15082 df-cat 15100 df-func 15181