Theorem dualcat2 15133

Description: The dual of a category is a category. Joy of cats 3.5

Hypotheses

Ref	Expression
dualcat2.1	|- D = (dom` T)
dualcat2.2	|- C = (cod` T)
dualcat2.3	|- J = (id` T)
dualcat2.4	|- R = (o` T)

Assertion

Ref	Expression
dualcat2	|- (T e. Cat -> <.<.C, D>., <.J, {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}>.>. e. Cat )

Distinct variable groups:   x,C,y,z   x,D,y,z   x,J,y,z   x,R,y,z   x,T,y,z

Proof of Theorem dualcat2

Step	Hyp	Ref	Expression
1		catded 15111	. . . 4 |- (T e. Cat -> T e. Ded )
2		dualcat2.1	. . . . 5 |- D = (dom` T)
3		dualcat2.2	. . . . 5 |- C = (cod` T)
4		dualcat2.3	. . . . 5 |- J = (id` T)
5		dualcat2.4	. . . . 5 |- R = (o` T)
6	2, 3, 4, 5	dualded 15132	. . . 4 |- (T e. Ded -> <.<.C, D>., <.J, {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}>.>. e. Ded )
7	1, 6	syl 12	. . 3 |- (T e. Cat -> <.<.C, D>., <.J, {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}>.>. e. Ded )
8		dedalg 15090	. . . . . . . . . . . . . . . . . . . . . 22 |- (T e. Ded -> T e. Alg )
9	2, 3	dcsda 15080	. . . . . . . . . . . . . . . . . . . . . . 23 |- (T e. Alg -> dom D = dom C)
10		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (dom D = dom C -> (h e. dom D <-> h e. dom C))
11		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (dom D = dom C -> (g e. dom D <-> g e. dom C))
12		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (dom D = dom C -> (f e. dom D <-> f e. dom C))
13	10, 11, 12	3anbi123d 1168	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (dom D = dom C -> ((h e. dom D /\ g e. dom D /\ f e. dom D) <-> (h e. dom C /\ g e. dom C /\ f e. dom C)))
14	13	biimprd 171	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (dom D = dom C -> ((h e. dom C /\ g e. dom C /\ f e. dom C) -> (h e. dom D /\ g e. dom D /\ f e. dom D)))
15		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- dom D = dom D
16	15, 2, 3, 5	cmpasso 15120	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((T e. Cat /\ (h e. dom D /\ g e. dom D /\ f e. dom D)) -> (((D` f) = (C` g) /\ (D` g) = (C` h)) -> (fR(gRh)) = ((fRg)Rh)))
17	16	ex 402	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (T e. Cat -> ((h e. dom D /\ g e. dom D /\ f e. dom D) -> (((D` f) = (C` g) /\ (D` g) = (C` h)) -> (fR(gRh)) = ((fRg)Rh))))
18	14, 17	syl9 71	. . . . . . . . . . . . . . . . . . . . . . 23 |- (dom D = dom C -> (T e. Cat -> ((h e. dom C /\ g e. dom C /\ f e. dom C) -> (((D` f) = (C` g) /\ (D` g) = (C` h)) -> (fR(gRh)) = ((fRg)Rh)))))
19	9, 18	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 |- (T e. Alg -> (T e. Cat -> ((h e. dom C /\ g e. dom C /\ f e. dom C) -> (((D` f) = (C` g) /\ (D` g) = (C` h)) -> (fR(gRh)) = ((fRg)Rh)))))
20	1, 8, 19	3syl 24	. . . . . . . . . . . . . . . . . . . . 21 |- (T e. Cat -> (T e. Cat -> ((h e. dom C /\ g e. dom C /\ f e. dom C) -> (((D` f) = (C` g) /\ (D` g) = (C` h)) -> (fR(gRh)) = ((fRg)Rh)))))
21	20	pm2.43i 78	. . . . . . . . . . . . . . . . . . . 20 |- (T e. Cat -> ((h e. dom C /\ g e. dom C /\ f e. dom C) -> (((D` f) = (C` g) /\ (D` g) = (C` h)) -> (fR(gRh)) = ((fRg)Rh))))
22	21	imp 377	. . . . . . . . . . . . . . . . . . 19 |- ((T e. Cat /\ (h e. dom C /\ g e. dom C /\ f e. dom C)) -> (((D` f) = (C` g) /\ (D` g) = (C` h)) -> (fR(gRh)) = ((fRg)Rh)))
23	22	com12 14	. . . . . . . . . . . . . . . . . 18 |- (((D` f) = (C` g) /\ (D` g) = (C` h)) -> ((T e. Cat /\ (h e. dom C /\ g e. dom C /\ f e. dom C)) -> (fR(gRh)) = ((fRg)Rh)))
24	23	ex 402	. . . . . . . . . . . . . . . . 17 |- ((D` f) = (C` g) -> ((D` g) = (C` h) -> ((T e. Cat /\ (h e. dom C /\ g e. dom C /\ f e. dom C)) -> (fR(gRh)) = ((fRg)Rh))))
25	24	eqcoms 1887	. . . . . . . . . . . . . . . 16 |- ((C` g) = (D` f) -> ((D` g) = (C` h) -> ((T e. Cat /\ (h e. dom C /\ g e. dom C /\ f e. dom C)) -> (fR(gRh)) = ((fRg)Rh))))
26	25	com12 14	. . . . . . . . . . . . . . 15 |- ((D` g) = (C` h) -> ((C` g) = (D` f) -> ((T e. Cat /\ (h e. dom C /\ g e. dom C /\ f e. dom C)) -> (fR(gRh)) = ((fRg)Rh))))
27	26	eqcoms 1887	. . . . . . . . . . . . . 14 |- ((C` h) = (D` g) -> ((C` g) = (D` f) -> ((T e. Cat /\ (h e. dom C /\ g e. dom C /\ f e. dom C)) -> (fR(gRh)) = ((fRg)Rh))))
28	27	imp 377	. . . . . . . . . . . . 13 |- (((C` h) = (D` g) /\ (C` g) = (D` f)) -> ((T e. Cat /\ (h e. dom C /\ g e. dom C /\ f e. dom C)) -> (fR(gRh)) = ((fRg)Rh)))
29	28	com12 14	. . . . . . . . . . . 12 |- ((T e. Cat /\ (h e. dom C /\ g e. dom C /\ f e. dom C)) -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (fR(gRh)) = ((fRg)Rh)))
30	29	3exp2 1086	. . . . . . . . . . 11 |- (T e. Cat -> (h e. dom C -> (g e. dom C -> (f e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (fR(gRh)) = ((fRg)Rh))))))
31	30	com24 41	. . . . . . . . . 10 |- (T e. Cat -> (f e. dom C -> (g e. dom C -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (fR(gRh)) = ((fRg)Rh))))))
32	31	imp32 390	. . . . . . . . 9 |- ((T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (fR(gRh)) = ((fRg)Rh))))
33	32	imp31 389	. . . . . . . 8 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (fR(gRh)) = ((fRg)Rh))
34		simp12 907	. . . . . . . . . . . . . . . . 17 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> T e. Cat )
35		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (dom C = dom D -> (h e. dom C <-> h e. dom D))
36		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (dom C = dom D -> (g e. dom C <-> g e. dom D))
37	35, 36	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (dom C = dom D -> ((h e. dom C /\ g e. dom C) <-> (h e. dom D /\ g e. dom D)))
38	37	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (dom D = dom C -> ((h e. dom C /\ g e. dom C) <-> (h e. dom D /\ g e. dom D)))
39	38	biimpcd 172	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((h e. dom C /\ g e. dom C) -> (dom D = dom C -> (h e. dom D /\ g e. dom D)))
40	39	ex 402	. . . . . . . . . . . . . . . . . . . . . . 23 |- (h e. dom C -> (g e. dom C -> (dom D = dom C -> (h e. dom D /\ g e. dom D))))
41	40	com3l 38	. . . . . . . . . . . . . . . . . . . . . 22 |- (g e. dom C -> (dom D = dom C -> (h e. dom C -> (h e. dom D /\ g e. dom D))))
42	41	adantl 424	. . . . . . . . . . . . . . . . . . . . 21 |- ((f e. dom C /\ g e. dom C) -> (dom D = dom C -> (h e. dom C -> (h e. dom D /\ g e. dom D))))
43	42	impcom 378	. . . . . . . . . . . . . . . . . . . 20 |- ((dom D = dom C /\ (f e. dom C /\ g e. dom C)) -> (h e. dom C -> (h e. dom D /\ g e. dom D)))
44	43	3adant2 895	. . . . . . . . . . . . . . . . . . 19 |- ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (h e. dom C -> (h e. dom D /\ g e. dom D)))
45	44	imp 377	. . . . . . . . . . . . . . . . . 18 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> (h e. dom D /\ g e. dom D))
46	45	3adant3 896	. . . . . . . . . . . . . . . . 17 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (h e. dom D /\ g e. dom D))
47		eqcom 1886	. . . . . . . . . . . . . . . . . . . 20 |- ((C` h) = (D` g) <-> (D` g) = (C` h))
48	47	biimpi 168	. . . . . . . . . . . . . . . . . . 19 |- ((C` h) = (D` g) -> (D` g) = (C` h))
49	48	adantr 425	. . . . . . . . . . . . . . . . . 18 |- (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (D` g) = (C` h))
50	49	3ad2ant3 899	. . . . . . . . . . . . . . . . 17 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (D` g) = (C` h))
51	34, 46, 50	3jca 1050	. . . . . . . . . . . . . . . 16 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (T e. Cat /\ (h e. dom D /\ g e. dom D) /\ (D` g) = (C` h)))
52	51	3exp 1066	. . . . . . . . . . . . . . 15 |- ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (T e. Cat /\ (h e. dom D /\ g e. dom D) /\ (D` g) = (C` h)))))
53	52	3exp 1066	. . . . . . . . . . . . . 14 |- (dom D = dom C -> (T e. Cat -> ((f e. dom C /\ g e. dom C) -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (T e. Cat /\ (h e. dom D /\ g e. dom D) /\ (D` g) = (C` h)))))))
54	9, 53	syl 12	. . . . . . . . . . . . 13 |- (T e. Alg -> (T e. Cat -> ((f e. dom C /\ g e. dom C) -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (T e. Cat /\ (h e. dom D /\ g e. dom D) /\ (D` g) = (C` h)))))))
55	1, 8, 54	3syl 24	. . . . . . . . . . . 12 |- (T e. Cat -> (T e. Cat -> ((f e. dom C /\ g e. dom C) -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (T e. Cat /\ (h e. dom D /\ g e. dom D) /\ (D` g) = (C` h)))))))
56	55	pm2.43i 78	. . . . . . . . . . 11 |- (T e. Cat -> ((f e. dom C /\ g e. dom C) -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (T e. Cat /\ (h e. dom D /\ g e. dom D) /\ (D` g) = (C` h))))))
57	56	imp41 395	. . . . . . . . . 10 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (T e. Cat /\ (h e. dom D /\ g e. dom D) /\ (D` g) = (C` h)))
58	2, 3, 5	dualcat2lem 15129	. . . . . . . . . 10 |- ((T e. Cat /\ (h e. dom D /\ g e. dom D) /\ (D` g) = (C` h)) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g) = (gRh))
59	57, 58	syl 12	. . . . . . . . 9 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g) = (gRh))
60		opreq1 4889	. . . . . . . . . 10 |- ((h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g) = (gRh) -> ((h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = ((gRh){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f))
61		simplll 452	. . . . . . . . . . 11 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> T e. Cat )
62		simpl2 880	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> T e. Cat )
63	35	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (dom C = dom D -> (h e. dom C -> h e. dom D))
64	63	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (dom D = dom C -> (h e. dom C -> h e. dom D))
65	64	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (h e. dom C -> h e. dom D))
66	65	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> h e. dom D)
67	36	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (dom C = dom D -> (g e. dom C -> g e. dom D))
68	67	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (dom D = dom C -> (g e. dom C -> g e. dom D))
69	68	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (g e. dom C -> (dom D = dom C -> g e. dom D))
70	69	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((f e. dom C /\ g e. dom C) -> (dom D = dom C -> g e. dom D))
71	70	impcom 378	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((dom D = dom C /\ (f e. dom C /\ g e. dom C)) -> g e. dom D)
72	71	3adant2 895	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> g e. dom D)
73	72	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> g e. dom D)
74	62, 66, 73	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> (T e. Cat /\ h e. dom D /\ g e. dom D))
75	74	ex 402	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (h e. dom C -> (T e. Cat /\ h e. dom D /\ g e. dom D)))
76	2	dmeqi 4158	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- dom D = dom (dom` T)
77	76, 2, 3, 5	cmpmorp 15126	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((T e. Cat /\ h e. dom D /\ g e. dom D) -> ((D` g) = (C` h) -> (gRh) e. dom D))
78	75, 77	syl6 25	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (h e. dom C -> ((D` g) = (C` h) -> (gRh) e. dom D)))
79	78	com13 37	. . . . . . . . . . . . . . . . . . . . . 22 |- ((D` g) = (C` h) -> (h e. dom C -> ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (gRh) e. dom D)))
80	79	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . 21 |- ((C` h) = (D` g) -> (h e. dom C -> ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (gRh) e. dom D)))
81	80	adantr 425	. . . . . . . . . . . . . . . . . . . 20 |- (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (h e. dom C -> ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (gRh) e. dom D)))
82	81	com13 37	. . . . . . . . . . . . . . . . . . 19 |- ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (gRh) e. dom D)))
83	82	3imp 1061	. . . . . . . . . . . . . . . . . 18 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (gRh) e. dom D)
84		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (dom C = dom D -> (f e. dom C <-> f e. dom D))
85	84	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (dom C = dom D -> (f e. dom C -> f e. dom D))
86	85	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . 23 |- (dom D = dom C -> (f e. dom C -> f e. dom D))
87	86	com12 14	. . . . . . . . . . . . . . . . . . . . . 22 |- (f e. dom C -> (dom D = dom C -> f e. dom D))
88	87	adantr 425	. . . . . . . . . . . . . . . . . . . . 21 |- ((f e. dom C /\ g e. dom C) -> (dom D = dom C -> f e. dom D))
89	88	impcom 378	. . . . . . . . . . . . . . . . . . . 20 |- ((dom D = dom C /\ (f e. dom C /\ g e. dom C)) -> f e. dom D)
90	89	3adant2 895	. . . . . . . . . . . . . . . . . . 19 |- ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> f e. dom D)
91	90	3ad2ant1 897	. . . . . . . . . . . . . . . . . 18 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> f e. dom D)
92	83, 91	jca 310	. . . . . . . . . . . . . . . . 17 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> ((gRh) e. dom D /\ f e. dom D))
93	92	3exp 1066	. . . . . . . . . . . . . . . 16 |- ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> ((gRh) e. dom D /\ f e. dom D))))
94	93	3exp 1066	. . . . . . . . . . . . . . 15 |- (dom D = dom C -> (T e. Cat -> ((f e. dom C /\ g e. dom C) -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> ((gRh) e. dom D /\ f e. dom D))))))
95	9, 94	syl 12	. . . . . . . . . . . . . 14 |- (T e. Alg -> (T e. Cat -> ((f e. dom C /\ g e. dom C) -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> ((gRh) e. dom D /\ f e. dom D))))))
96	1, 8, 95	3syl 24	. . . . . . . . . . . . 13 |- (T e. Cat -> (T e. Cat -> ((f e. dom C /\ g e. dom C) -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> ((gRh) e. dom D /\ f e. dom D))))))
97	96	pm2.43i 78	. . . . . . . . . . . 12 |- (T e. Cat -> ((f e. dom C /\ g e. dom C) -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> ((gRh) e. dom D /\ f e. dom D)))))
98	97	imp41 395	. . . . . . . . . . 11 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> ((gRh) e. dom D /\ f e. dom D))
99		id 73	. . . . . . . . . . . . . 14 |- ((D` f) = (C` g) -> (D` f) = (C` g))
100	99	eqcoms 1887	. . . . . . . . . . . . 13 |- ((C` g) = (D` f) -> (D` f) = (C` g))
101	100	ad2antll 443	. . . . . . . . . . . 12 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (D` f) = (C` g))
102	35	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (dom D = dom C -> (h e. dom C <-> h e. dom D))
103	102	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (h e. dom C <-> h e. dom D))
104	103	biimpa 460	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> h e. dom D)
105	68	adantld 426	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (dom D = dom C -> ((f e. dom C /\ g e. dom C) -> g e. dom D))
106	105	a1d 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (dom D = dom C -> (T e. Cat -> ((f e. dom C /\ g e. dom C) -> g e. dom D)))
107	106	3imp 1061	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) -> g e. dom D)
108	107	adantr 425	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> g e. dom D)
109	62, 104, 108	3jca 1050	. . . . . . . . . . . . . . . . . . . . . 22 |- (((dom D = dom C /\ T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> (T e. Cat /\ h e. dom D /\ g e. dom D))
110	109	3exp1 1084	. . . . . . . . . . . . . . . . . . . . 21 |- (dom D = dom C -> (T e. Cat -> ((f e. dom C /\ g e. dom C) -> (h e. dom C -> (T e. Cat /\ h e. dom D /\ g e. dom D)))))
111	9, 110	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (T e. Alg -> (T e. Cat -> ((f e. dom C /\ g e. dom C) -> (h e. dom C -> (T e. Cat /\ h e. dom D /\ g e. dom D)))))
112	1, 8, 111	3syl 24	. . . . . . . . . . . . . . . . . . 19 |- (T e. Cat -> (T e. Cat -> ((f e. dom C /\ g e. dom C) -> (h e. dom C -> (T e. Cat /\ h e. dom D /\ g e. dom D)))))
113	112	pm2.43i 78	. . . . . . . . . . . . . . . . . 18 |- (T e. Cat -> ((f e. dom C /\ g e. dom C) -> (h e. dom C -> (T e. Cat /\ h e. dom D /\ g e. dom D))))
114	113	imp31 389	. . . . . . . . . . . . . . . . 17 |- (((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> (T e. Cat /\ h e. dom D /\ g e. dom D))
115	15, 2, 3, 5	codcmpc 15119	. . . . . . . . . . . . . . . . 17 |- ((T e. Cat /\ h e. dom D /\ g e. dom D) -> ((D` g) = (C` h) -> (C` (gRh)) = (C` g)))
116	114, 115	syl 12	. . . . . . . . . . . . . . . 16 |- (((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> ((D` g) = (C` h) -> (C` (gRh)) = (C` g)))
117	116	com12 14	. . . . . . . . . . . . . . 15 |- ((D` g) = (C` h) -> (((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> (C` (gRh)) = (C` g)))
118	117	eqcoms 1887	. . . . . . . . . . . . . 14 |- ((C` h) = (D` g) -> (((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> (C` (gRh)) = (C` g)))
119	118	adantr 425	. . . . . . . . . . . . 13 |- (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> (C` (gRh)) = (C` g)))
120	119	impcom 378	. . . . . . . . . . . 12 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (C` (gRh)) = (C` g))
121	101, 120	eqtr4d 1928	. . . . . . . . . . 11 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (D` f) = (C` (gRh)))
122	2, 3, 5	dualcat2lem 15129	. . . . . . . . . . 11 |- ((T e. Cat /\ ((gRh) e. dom D /\ f e. dom D) /\ (D` f) = (C` (gRh))) -> ((gRh){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = (fR(gRh)))
123	61, 98, 121, 122	syl111anc 1100	. . . . . . . . . 10 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> ((gRh){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = (fR(gRh)))
124	60, 123	sylan9eqr 1951	. . . . . . . . 9 |- (((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) /\ (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g) = (gRh)) -> ((h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = (fR(gRh)))
125	59, 124	mpdan 768	. . . . . . . 8 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> ((h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = (fR(gRh)))
126	9	eqcomd 1889	. . . . . . . . . . . . . . . 16 |- (T e. Alg -> dom C = dom D)
127	126	eleq2d 1964	. . . . . . . . . . . . . . 15 |- (T e. Alg -> (g e. dom C <-> g e. dom D))
128	1, 8, 127	3syl 24	. . . . . . . . . . . . . 14 |- (T e. Cat -> (g e. dom C <-> g e. dom D))
129	128	biimpcd 172	. . . . . . . . . . . . 13 |- (g e. dom C -> (T e. Cat -> g e. dom D))
130	129	adantl 424	. . . . . . . . . . . 12 |- ((f e. dom C /\ g e. dom C) -> (T e. Cat -> g e. dom D))
131	130	impcom 378	. . . . . . . . . . 11 |- ((T e. Cat /\ (f e. dom C /\ g e. dom C)) -> g e. dom D)
132	131	ad2antrr 440	. . . . . . . . . 10 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> g e. dom D)
133	1, 8, 126	3syl 24	. . . . . . . . . . . . . . 15 |- (T e. Cat -> dom C = dom D)
134	133	eleq2d 1964	. . . . . . . . . . . . . 14 |- (T e. Cat -> (f e. dom C <-> f e. dom D))
135	134	biimpcd 172	. . . . . . . . . . . . 13 |- (f e. dom C -> (T e. Cat -> f e. dom D))
136	135	adantr 425	. . . . . . . . . . . 12 |- ((f e. dom C /\ g e. dom C) -> (T e. Cat -> f e. dom D))
137	136	impcom 378	. . . . . . . . . . 11 |- ((T e. Cat /\ (f e. dom C /\ g e. dom C)) -> f e. dom D)
138	137	ad2antrr 440	. . . . . . . . . 10 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> f e. dom D)
139		eqcom 1886	. . . . . . . . . . . 12 |- ((C` g) = (D` f) <-> (D` f) = (C` g))
140	139	biimpi 168	. . . . . . . . . . 11 |- ((C` g) = (D` f) -> (D` f) = (C` g))
141	140	ad2antll 443	. . . . . . . . . 10 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (D` f) = (C` g))
142	2, 3, 5	dualcat2lem 15129	. . . . . . . . . 10 |- ((T e. Cat /\ (g e. dom D /\ f e. dom D) /\ (D` f) = (C` g)) -> (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = (fRg))
143	61, 132, 138, 141, 142	syl121anc 1105	. . . . . . . . 9 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = (fRg))
144		opreq2 4890	. . . . . . . . . 10 |- ((g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = (fRg) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f)) = (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (fRg)))
145	133	eleq2d 1964	. . . . . . . . . . . . . . 15 |- (T e. Cat -> (h e. dom C <-> h e. dom D))
146	145	biimpd 170	. . . . . . . . . . . . . 14 |- (T e. Cat -> (h e. dom C -> h e. dom D))
147	146	adantr 425	. . . . . . . . . . . . 13 |- ((T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (h e. dom C -> h e. dom D))
148	147	imp 377	. . . . . . . . . . . 12 |- (((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> h e. dom D)
149	148	adantr 425	. . . . . . . . . . 11 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> h e. dom D)
150		simpl 346	. . . . . . . . . . . . . 14 |- ((T e. Cat /\ (f e. dom C /\ g e. dom C)) -> T e. Cat )
151	150, 131, 137	3jca 1050	. . . . . . . . . . . . 13 |- ((T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (T e. Cat /\ g e. dom D /\ f e. dom D))
152	151	ad2antrr 440	. . . . . . . . . . . 12 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (T e. Cat /\ g e. dom D /\ f e. dom D))
153	76, 2, 3, 5	cmpmorp 15126	. . . . . . . . . . . 12 |- ((T e. Cat /\ g e. dom D /\ f e. dom D) -> ((D` f) = (C` g) -> (fRg) e. dom D))
154	152, 141, 153	sylc 83	. . . . . . . . . . 11 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (fRg) e. dom D)
155	15, 2, 3, 5	domcmpc 15118	. . . . . . . . . . . . . 14 |- ((T e. Cat /\ g e. dom D /\ f e. dom D) -> ((D` f) = (C` g) -> (D` (fRg)) = (D` g)))
156	155	imp 377	. . . . . . . . . . . . 13 |- (((T e. Cat /\ g e. dom D /\ f e. dom D) /\ (D` f) = (C` g)) -> (D` (fRg)) = (D` g))
157		simpll 448	. . . . . . . . . . . . . 14 |- (((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> T e. Cat )
158	131	adantr 425	. . . . . . . . . . . . . 14 |- (((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> g e. dom D)
159	137	adantr 425	. . . . . . . . . . . . . 14 |- (((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> f e. dom D)
160	157, 158, 159	3jca 1050	. . . . . . . . . . . . 13 |- (((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) -> (T e. Cat /\ g e. dom D /\ f e. dom D))
161	140	adantl 424	. . . . . . . . . . . . 13 |- (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (D` f) = (C` g))
162	156, 160, 161	syl2an 503	. . . . . . . . . . . 12 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (D` (fRg)) = (D` g))
163	48	ad2antrl 442	. . . . . . . . . . . 12 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (D` g) = (C` h))
164	162, 163	eqtrd 1925	. . . . . . . . . . 11 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (D` (fRg)) = (C` h))
165	2, 3, 5	dualcat2lem 15129	. . . . . . . . . . 11 |- ((T e. Cat /\ (h e. dom D /\ (fRg) e. dom D) /\ (D` (fRg)) = (C` h)) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (fRg)) = ((fRg)Rh))
166	61, 149, 154, 164, 165	syl121anc 1105	. . . . . . . . . 10 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (fRg)) = ((fRg)Rh))
167	144, 166	sylan9eqr 1951	. . . . . . . . 9 |- (((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) /\ (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = (fRg)) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f)) = ((fRg)Rh))
168	143, 167	mpdan 768	. . . . . . . 8 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f)) = ((fRg)Rh))
169	33, 125, 168	3eqtr4rd 1939	. . . . . . 7 |- ((((T e. Cat /\ (f e. dom C /\ g e. dom C)) /\ h e. dom C) /\ ((C` h) = (D` g) /\ (C` g) = (D` f))) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f)) = ((h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f))
170	169	exp31 407	. . . . . 6 |- ((T e. Cat /\ (f e. dom C /\ g e. dom C)) -> (h e. dom C -> (((C` h) = (D` g) /\ (C` g) = (D` f)) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f)) = ((h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f))))
171	170	r19.21aiv 2175	. . . . 5 |- ((T e. Cat /\ (f e. dom C /\ g e. dom C)) -> A.h e. dom C(((C` h) = (D` g) /\ (C` g) = (D` f)) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f)) = ((h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f)))
172	171	ex 402	. . . 4 |- (T e. Cat -> ((f e. dom C /\ g e. dom C) -> A.h e. dom C(((C` h) = (D` g) /\ (C` g) = (D` f)) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f)) = ((h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f))))
173	172	r19.21aivv 2183	. . 3 |- (T e. Cat -> A.f e. dom CA.g e. dom CA.h e. dom C(((C` h) = (D` g) /\ (C` g) = (D` f)) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f)) = ((h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f)))
174		simpll 448	. . . . . . . 8 |- (((T e. Cat /\ (a e. dom J /\ f e. dom C)) /\ (D` f) = a) -> T e. Cat )
175	4	dmeqi 4158	. . . . . . . . . . 11 |- dom J = dom (id` T)
176	76, 175, 4	jdmo 15125	. . . . . . . . . 10 |- ((T e. Cat /\ a e. dom J) -> (J` a) e. dom D)
177	176	adantrr 431	. . . . . . . . 9 |- ((T e. Cat /\ (a e. dom J /\ f e. dom C)) -> (J` a) e. dom D)
178	177	adantr 425	. . . . . . . 8 |- (((T e. Cat /\ (a e. dom J /\ f e. dom C)) /\ (D` f) = a) -> (J` a) e. dom D)
179	135	adantl 424	. . . . . . . . . 10 |- ((a e. dom J /\ f e. dom C) -> (T e. Cat -> f e. dom D))
180	179	impcom 378	. . . . . . . . 9 |- ((T e. Cat /\ (a e. dom J /\ f e. dom C)) -> f e. dom D)
181	180	adantr 425	. . . . . . . 8 |- (((T e. Cat /\ (a e. dom J /\ f e. dom C)) /\ (D` f) = a) -> f e. dom D)
182		simpr 350	. . . . . . . . 9 |- (((T e. Cat /\ (a e. dom J /\ f e. dom C)) /\ (D` f) = a) -> (D` f) = a)
183		simplrl 454	. . . . . . . . . . 11 |- (((T e. Cat /\ (a e. dom J /\ f e. dom C)) /\ (D` f) = a) -> a e. dom J)
184		eqid 1884	. . . . . . . . . . . 12 |- dom J = dom J
185	184, 2, 4, 3	idosc 15116	. . . . . . . . . . 11 |- ((T e. Cat /\ a e. dom J) -> ((D` (J` a)) = a /\ (C` (J` a)) = a))
186	174, 183, 185	syl11anc 524	. . . . . . . . . 10 |- (((T e. Cat /\ (a e. dom J /\ f e. dom C)) /\ (D` f) = a) -> ((D` (J` a)) = a /\ (C` (J` a)) = a))
187	186	simprd 352	. . . . . . . . 9 |- (((T e. Cat /\ (a e. dom J /\ f e. dom C)) /\ (D` f) = a) -> (C` (J` a)) = a)
188	182, 187	eqtr4d 1928	. . . . . . . 8 |- (((T e. Cat /\ (a e. dom J /\ f e. dom C)) /\ (D` f) = a) -> (D` f) = (C` (J` a)))
189	2, 3, 5	dualcat2lem 15129	. . . . . . . 8 |- ((T e. Cat /\ ((J` a) e. dom D /\ f e. dom D) /\ (D` f) = (C` (J` a))) -> ((J` a){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = (fR(J` a)))
190	174, 178, 181, 188, 189	syl121anc 1105	. . . . . . 7 |- (((T e. Cat /\ (a e. dom J /\ f e. dom C)) /\ (D` f) = a) -> ((J` a){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = (fR(J` a)))
191		simpl 346	. . . . . . . . 9 |- ((T e. Cat /\ (a e. dom J /\ f e. dom C)) -> T e. Cat )
192		simprl 450	. . . . . . . . 9 |- ((T e. Cat /\ (a e. dom J /\ f e. dom C)) -> a e. dom J)
193	1, 8	syl 12	. . . . . . . . . . . . . . 15 |- (T e. Cat -> T e. Alg )
194	193, 9	syl 12	. . . . . . . . . . . . . 14 |- (T e. Cat -> dom D = dom C)
195	194	eqcomd 1889	. . . . . . . . . . . . 13 |- (T e. Cat -> dom C = dom D)
196	195	eleq2d 1964	. . . . . . . . . . . 12 |- (T e. Cat -> (f e. dom C <-> f e. dom D))
197	196	biimpcd 172	. . . . . . . . . . 11 |- (f e. dom C -> (T e. Cat -> f e. dom D))
198	197	adantl 424	. . . . . . . . . 10 |- ((a e. dom J /\ f e. dom C) -> (T e. Cat -> f e. dom D))
199	198	impcom 378	. . . . . . . . 9 |- ((T e. Cat /\ (a e. dom J /\ f e. dom C)) -> f e. dom D)
200	15, 2, 184, 4, 5	cmpidb 15122	. . . . . . . . 9 |- ((T e. Cat /\ a e. dom J /\ f e. dom D) -> ((D` f) = a -> (fR(J` a)) = f))
201	191, 192, 199, 200	syl111anc 1100	. . . . . . . 8 |- ((T e. Cat /\ (a e. dom J /\ f e. dom C)) -> ((D` f) = a -> (fR(J` a)) = f))
202	201	imp 377	. . . . . . 7 |- (((T e. Cat /\ (a e. dom J /\ f e. dom C)) /\ (D` f) = a) -> (fR(J` a)) = f)
203	190, 202	eqtrd 1925	. . . . . 6 |- (((T e. Cat /\ (a e. dom J /\ f e. dom C)) /\ (D` f) = a) -> ((J` a){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = f)
204	203	exp31 407	. . . . 5 |- (T e. Cat -> ((a e. dom J /\ f e. dom C) -> ((D` f) = a -> ((J` a){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = f)))
205	204	r19.21aivv 2183	. . . 4 |- (T e. Cat -> A.a e. dom JA.f e. dom C((D` f) = a -> ((J` a){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = f))
206	15, 2, 184, 4, 5, 3	cmpida 15121	. . . . . . 7 |- ((T e. Cat /\ a e. dom J /\ f e. dom D) -> ((C` f) = a -> ((J` a)Rf) = f))
207	206	3expib 1070	. . . . . 6 |- (T e. Cat -> ((a e. dom J /\ f e. dom D) -> ((C` f) = a -> ((J` a)Rf) = f)))
208	134	anbi2d 678	. . . . . . . 8 |- (T e. Cat -> ((a e. dom J /\ f e. dom C) <-> (a e. dom J /\ f e. dom D)))
209	208	imbi1d 675	. . . . . . 7 |- (T e. Cat -> (((a e. dom J /\ f e. dom C) -> ((C` f) = a -> (f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = f)) <-> ((a e. dom J /\ f e. dom D) -> ((C` f) = a -> (f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = f))))
210		simpll 448	. . . . . . . . . . 11 |- (((T e. Cat /\ (a e. dom J /\ f e. dom D)) /\ (C` f) = a) -> T e. Cat )
211		simplrr 455	. . . . . . . . . . 11 |- (((T e. Cat /\ (a e. dom J /\ f e. dom D)) /\ (C` f) = a) -> f e. dom D)
212	176	adantrr 431	. . . . . . . . . . . 12 |- ((T e. Cat /\ (a e. dom J /\ f e. dom D)) -> (J` a) e. dom D)
213	212	adantr 425	. . . . . . . . . . 11 |- (((T e. Cat /\ (a e. dom J /\ f e. dom D)) /\ (C` f) = a) -> (J` a) e. dom D)
214		eqtr3 1907	. . . . . . . . . . . 12 |- (((D` (J` a)) = a /\ (C` f) = a) -> (D` (J` a)) = (C` f))
215	185	simplld 348	. . . . . . . . . . . . 13 |- ((T e. Cat /\ a e. dom J) -> (D` (J` a)) = a)
216	215	adantrr 431	. . . . . . . . . . . 12 |- ((T e. Cat /\ (a e. dom J /\ f e. dom D)) -> (D` (J` a)) = a)
217	214, 216	sylan 497	. . . . . . . . . . 11 |- (((T e. Cat /\ (a e. dom J /\ f e. dom D)) /\ (C` f) = a) -> (D` (J` a)) = (C` f))
218	2, 3, 5	dualcat2lem 15129	. . . . . . . . . . 11 |- ((T e. Cat /\ (f e. dom D /\ (J` a) e. dom D) /\ (D` (J` a)) = (C` f)) -> (f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = ((J` a)Rf))
219	210, 211, 213, 217, 218	syl121anc 1105	. . . . . . . . . 10 |- (((T e. Cat /\ (a e. dom J /\ f e. dom D)) /\ (C` f) = a) -> (f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = ((J` a)Rf))
220	219	eqeq1d 1892	. . . . . . . . 9 |- (((T e. Cat /\ (a e. dom J /\ f e. dom D)) /\ (C` f) = a) -> ((f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = f <-> ((J` a)Rf) = f))
221	220	pm5.74da 646	. . . . . . . 8 |- ((T e. Cat /\ (a e. dom J /\ f e. dom D)) -> (((C` f) = a -> (f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = f) <-> ((C` f) = a -> ((J` a)Rf) = f)))
222	221	pm5.74da 646	. . . . . . 7 |- (T e. Cat -> (((a e. dom J /\ f e. dom D) -> ((C` f) = a -> (f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = f)) <-> ((a e. dom J /\ f e. dom D) -> ((C` f) = a -> ((J` a)Rf) = f))))
223	209, 222	bitrd 587	. . . . . 6 |- (T e. Cat -> (((a e. dom J /\ f e. dom C) -> ((C` f) = a -> (f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = f)) <-> ((a e. dom J /\ f e. dom D) -> ((C` f) = a -> ((J` a)Rf) = f))))
224	207, 223	mpbird 213	. . . . 5 |- (T e. Cat -> ((a e. dom J /\ f e. dom C) -> ((C` f) = a -> (f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = f)))
225	224	r19.21aivv 2183	. . . 4 |- (T e. Cat -> A.a e. dom JA.f e. dom C((C` f) = a -> (f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = f))
226	205, 225	jca 310	. . 3 |- (T e. Cat -> (A.a e. dom JA.f e. dom C((D` f) = a -> ((J` a){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = f) /\ A.a e. dom JA.f e. dom C((C` f) = a -> (f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = f)))
227	7, 173, 226	jca31 311	. 2 |- (T e. Cat -> ((<.<.C, D>., <.J, {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}>.>. e. Ded /\ A.f e. dom CA.g e. dom CA.h e. dom C(((C` h) = (D` g) /\ (C` g) = (D` f)) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f)) = ((h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f))) /\ (A.a e. dom JA.f e. dom C((D` f) = a -> ((J` a){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = f) /\ A.a e. dom JA.f e. dom C((C` f) = a -> (f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = f))))
228		eqid 1884	. . . 4 |- dom C = dom C
229	228, 184	iscat 15101	. . 3 |- (((C e. _V /\ D e. _V /\ J e. _V) /\ {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} e. _V) -> (<.<.C, D>., <.J, {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}>.>. e. Cat <-> ((<.<.C, D>., <.J, {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}>.>. e. Ded /\ A.f e. dom CA.g e. dom CA.h e. dom C(((C` h) = (D` g) /\ (C` g) = (D` f)) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f)) = ((h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f))) /\ (A.a e. dom JA.f e. dom C((D` f) = a -> ((J` a){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = f) /\ A.a e. dom JA.f e. dom C((C` f) = a -> (f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = f)))))
230	3	eleq1i 1960	. . . . 5 |- (C e. _V <-> (cod` T) e. _V)
231	2	eleq1i 1960	. . . . 5 |- (D e. _V <-> (dom` T) e. _V)
232	4	eleq1i 1960	. . . . 5 |- (J e. _V <-> (id` T) e. _V)
233	230, 231, 232	3anbi123i 1056	. . . 4 |- ((C e. _V /\ D e. _V /\ J e. _V) <-> ((cod` T) e. _V /\ (dom` T) e. _V /\ (id` T) e. _V))
234		fvex 4689	. . . 4 |- (cod` T) e. _V
235		fvex 4689	. . . 4 |- (dom` T) e. _V
236		fvex 4689	. . . 4 |- (id` T) e. _V
237	233, 234, 235, 236	mpbir3an 1052	. . 3 |- (C e. _V /\ D e. _V /\ J e. _V)
238		ssexg 3457	. . . 4 |- (({<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} C_ {<.<.x, y>., z>. | (<.y, x>. e. (dom D X. dom D) /\ z = (yRx))} /\ {<.<.x, y>., z>. | (<.y, x>. e. (dom D X. dom D) /\ z = (yRx))} e. _V) -> {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} e. _V)
239	15, 2, 5	cmppfc 15115	. . . . . . . 8 |- (T e. Cat -> (Fun R /\ dom R C_ (dom D X. dom D) /\ ran R C_ dom D))
240	239	simp2d 889	. . . . . . 7 |- (T e. Cat -> dom R C_ (dom D X. dom D))
241	240	sseld 2619	. . . . . 6 |- (T e. Cat -> (<.y, x>. e. dom R -> <.y, x>. e. (dom D X. dom D)))
242	241	anim1d 619	. . . . 5 |- (T e. Cat -> ((<.y, x>. e. dom R /\ z = (yRx)) -> (<.y, x>. e. (dom D X. dom D) /\ z = (yRx))))
243	242	ssoprab2g 14333	. . . 4 |- (T e. Cat -> {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} C_ {<.<.x, y>., z>. | (<.y, x>. e. (dom D X. dom D) /\ z = (yRx))})
244	235	dmex 4208	. . . . . . 7 |- dom (dom` T) e. _V
245	76, 244	eqeltri 1967	. . . . . 6 |- dom D e. _V
246		eqid 1884	. . . . . 6 |- {<.<.x, y>., z>. | ((x e. dom D /\ y e. dom D) /\ z = (yRx))} = {<.<.x, y>., z>. | ((x e. dom D /\ y e. dom D) /\ z = (yRx))}
247	245, 245, 246	oprabex2 4950	. . . . 5 |- {<.<.x, y>., z>. | ((x e. dom D /\ y e. dom D) /\ z = (yRx))} e. _V
248		cnvxp 4332	. . . . . . . . . . . 12 |- `'(dom D X. dom D) = (dom D X. dom D)
249	248	eqcomi 1888	. . . . . . . . . . 11 |- (dom D X. dom D) = `'(dom D X. dom D)
250	249	eleq2i 1961	. . . . . . . . . 10 |- (<.y, x>. e. (dom D X. dom D) <-> <.y, x>. e. `'(dom D X. dom D))
251		visset 2295	. . . . . . . . . . 11 |- y e. _V
252		visset 2295	. . . . . . . . . . 11 |- x e. _V
253	251, 252	opelcnv 4143	. . . . . . . . . 10 |- (<.y, x>. e. `'(dom D X. dom D) <-> <.x, y>. e. (dom D X. dom D))
254	250, 253	bitri 190	. . . . . . . . 9 |- (<.y, x>. e. (dom D X. dom D) <-> <.x, y>. e. (dom D X. dom D))
255	254	anbi1i 539	. . . . . . . 8 |- ((<.y, x>. e. (dom D X. dom D) /\ z = (yRx)) <-> (<.x, y>. e. (dom D X. dom D) /\ z = (yRx)))
256	255	oprabbii 4923	. . . . . . 7 |- {<.<.x, y>., z>. | (<.y, x>. e. (dom D X. dom D) /\ z = (yRx))} = {<.<.x, y>., z>. | (<.x, y>. e. (dom D X. dom D) /\ z = (yRx))}
257	256	eleq1i 1960	. . . . . 6 |- ({<.<.x, y>., z>. | (<.y, x>. e. (dom D X. dom D) /\ z = (yRx))} e. _V <-> {<.<.x, y>., z>. | (<.x, y>. e. (dom D X. dom D) /\ z = (yRx))} e. _V)
258		twsvbdop 14332	. . . . . . 7 |- {<.<.x, y>., z>. | (<.x, y>. e. (dom D X. dom D) /\ z = (yRx))} = {<.<.x, y>., z>. | ((x e. dom D /\ y e. dom D) /\ z = (yRx))}
259	258	eleq1i 1960	. . . . . 6 |- ({<.<.x, y>., z>. | (<.x, y>. e. (dom D X. dom D) /\ z = (yRx))} e. _V <-> {<.<.x, y>., z>. | ((x e. dom D /\ y e. dom D) /\ z = (yRx))} e. _V)
260	257, 259	bitri 190	. . . . 5 |- ({<.<.x, y>., z>. | (<.y, x>. e. (dom D X. dom D) /\ z = (yRx))} e. _V <-> {<.<.x, y>., z>. | ((x e. dom D /\ y e. dom D) /\ z = (yRx))} e. _V)
261	247, 260	mpbir 207	. . . 4 |- {<.<.x, y>., z>. | (<.y, x>. e. (dom D X. dom D) /\ z = (yRx))} e. _V
262	238, 243, 261	sylancl 525	. . 3 |- (T e. Cat -> {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} e. _V)
263	229, 237, 262	sylancr 526	. 2 |- (T e. Cat -> (<.<.C, D>., <.J, {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}>.>. e. Cat <-> ((<.<.C, D>., <.J, {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}>.>. e. Ded /\ A.f e. dom CA.g e. dom CA.h e. dom C(((C` h) = (D` g) /\ (C` g) = (D` f)) -> (h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (g{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f)) = ((h{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}g){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f))) /\ (A.a e. dom JA.f e. dom C((D` f) = a -> ((J` a){<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}f) = f) /\ A.a e. dom JA.f e. dom C((C` f) = a -> (f{<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} (J` a)) = f)))))
264	227, 263	mpbird 213	1 |- (T e. Cat -> <.<.C, D>., <.J, {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}>.>. e. Cat )

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292   C_ wss 2593  <.cop 3046   X. cxp 3984  `'ccnv 3985  dom cdm 3986  ran crn 3987  Fun wfun 3992  ` cfv 3998  (class class class)co 4884  {copab2 4885   Alg calg 15058  domcdom_ 15059  codccod_ 15060  idcid_ 15061  oco_ 15062   Ded cded 15081   Cat ccat 15099

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-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-fo 4012  df-fv 4014  df-opr 4886  df-oprab 4887  df-1st 5020  df-2nd 5021  df-alg 15063  df-doma 15064  df-coda 15065  df-ida 15066  df-cmpa 15067  df-ded 15082  df-cat 15100

Copyright terms: Public domain