Theorem dualalg 15131

Description: The dual of a Alg is a Alg.

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
dualalg	|- (T e. Alg -> <.<.C, D>., <.J, {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}>.>. e. Alg )

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

Proof of Theorem dualalg

Step	Hyp	Ref	Expression
1		visset 2295	. . . . . . . 8 |- x e. _V
2		visset 2295	. . . . . . . 8 |- y e. _V
3		opelcnvg 4140	. . . . . . . . 9 |- ((x e. _V /\ y e. _V) -> (<.x, y>. e. `'dom R <-> <.y, x>. e. dom R))
4	3	bicomd 580	. . . . . . . 8 |- ((x e. _V /\ y e. _V) -> (<.y, x>. e. dom R <-> <.x, y>. e. `'dom R))
5	1, 2, 4	mp2an 761	. . . . . . 7 |- (<.y, x>. e. dom R <-> <.x, y>. e. `'dom R)
6	5	a1i 8	. . . . . 6 |- (T e. Alg -> (<.y, x>. e. dom R <-> <.x, y>. e. `'dom R))
7	6	anbi1d 679	. . . . 5 |- (T e. Alg -> ((<.y, x>. e. dom R /\ z = (yRx)) <-> (<.x, y>. e. `'dom R /\ z = (yRx))))
8	7	oprabbidv 4922	. . . 4 |- (T e. Alg -> {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))} = {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))})
9	8	opeq2d 3165	. . 3 |- (T e. Alg -> <.J, {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}>. = <.J, {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))}>.)
10	9	opeq2d 3165	. 2 |- (T e. Alg -> <.<.C, D>., <.J, {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}>.>. = <.<.C, D>., <.J, {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))}>.>.)
11		dualcat2.1	. . . . 5 |- D = (dom` T)
12		dualcat2.2	. . . . 5 |- C = (cod` T)
13	11, 12	dcsda 15080	. . . 4 |- (T e. Alg -> dom D = dom C)
14		dualcat2.3	. . . . 5 |- J = (id` T)
15		dualcat2.4	. . . . 5 |- R = (o` T)
16		eqid 1884	. . . . 5 |- dom D = dom D
17		eqid 1884	. . . . 5 |- dom J = dom J
18	11, 12, 14, 15, 16, 17	algi 15074	. . . 4 |- (T e. Alg -> ((D:dom D-->dom J /\ C:dom D-->dom J /\ J:dom J-->dom D) /\ (Fun R /\ dom R C_ (dom D X. dom D) /\ ran R C_ dom D)))
19		feq2 4552	. . . . . . . 8 |- (dom D = dom C -> (D:dom D-->dom J <-> D:dom C-->dom J))
20	19	biimpd 170	. . . . . . 7 |- (dom D = dom C -> (D:dom D-->dom J -> D:dom C-->dom J))
21		feq2 4552	. . . . . . . 8 |- (dom D = dom C -> (C:dom D-->dom J <-> C:dom C-->dom J))
22	21	biimpd 170	. . . . . . 7 |- (dom D = dom C -> (C:dom D-->dom J -> C:dom C-->dom J))
23		feq3 4553	. . . . . . . 8 |- (dom D = dom C -> (J:dom J-->dom D <-> J:dom J-->dom C))
24	23	biimpd 170	. . . . . . 7 |- (dom D = dom C -> (J:dom J-->dom D -> J:dom J-->dom C))
25	20, 22, 24	3anim123d 1175	. . . . . 6 |- (dom D = dom C -> ((D:dom D-->dom J /\ C:dom D-->dom J /\ J:dom J-->dom D) -> (D:dom C-->dom J /\ C:dom C-->dom J /\ J:dom J-->dom C)))
26		idd 75	. . . . . . 7 |- (dom D = dom C -> (Fun R -> Fun R))
27		xpeq12 4020	. . . . . . . . 9 |- ((dom D = dom C /\ dom D = dom C) -> (dom D X. dom D) = (dom C X. dom C))
28	27	anidms 480	. . . . . . . 8 |- (dom D = dom C -> (dom D X. dom D) = (dom C X. dom C))
29		sseq2 2639	. . . . . . . . 9 |- ((dom D X. dom D) = (dom C X. dom C) -> (dom R C_ (dom D X. dom D) <-> dom R C_ (dom C X. dom C)))
30	29	biimpd 170	. . . . . . . 8 |- ((dom D X. dom D) = (dom C X. dom C) -> (dom R C_ (dom D X. dom D) -> dom R C_ (dom C X. dom C)))
31	28, 30	syl 12	. . . . . . 7 |- (dom D = dom C -> (dom R C_ (dom D X. dom D) -> dom R C_ (dom C X. dom C)))
32		sseq2 2639	. . . . . . . 8 |- (dom D = dom C -> (ran R C_ dom D <-> ran R C_ dom C))
33	32	biimpd 170	. . . . . . 7 |- (dom D = dom C -> (ran R C_ dom D -> ran R C_ dom C))
34	26, 31, 33	3anim123d 1175	. . . . . 6 |- (dom D = dom C -> ((Fun R /\ dom R C_ (dom D X. dom D) /\ ran R C_ dom D) -> (Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C)))
35	25, 34	anim12d 617	. . . . 5 |- (dom D = dom C -> (((D:dom D-->dom J /\ C:dom D-->dom J /\ J:dom J-->dom D) /\ (Fun R /\ dom R C_ (dom D X. dom D) /\ ran R C_ dom D)) -> ((D:dom C-->dom J /\ C:dom C-->dom J /\ J:dom J-->dom C) /\ (Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C))))
36		simp2 877	. . . . . . 7 |- ((D:dom C-->dom J /\ C:dom C-->dom J /\ J:dom J-->dom C) -> C:dom C-->dom J)
37		simp1 876	. . . . . . 7 |- ((D:dom C-->dom J /\ C:dom C-->dom J /\ J:dom J-->dom C) -> D:dom C-->dom J)
38		simp3 878	. . . . . . 7 |- ((D:dom C-->dom J /\ C:dom C-->dom J /\ J:dom J-->dom C) -> J:dom J-->dom C)
39	36, 37, 38	3jca 1050	. . . . . 6 |- ((D:dom C-->dom J /\ C:dom C-->dom J /\ J:dom J-->dom C) -> (C:dom C-->dom J /\ D:dom C-->dom J /\ J:dom J-->dom C))
40		cnvss 4134	. . . . . . . . . . . 12 |- (dom R C_ (dom C X. dom C) -> `'dom R C_ `'(dom C X. dom C))
41		sqpsym 14382	. . . . . . . . . . . . 13 |- `'(dom C X. dom C) C_ (dom C X. dom C)
42		sstr2 2623	. . . . . . . . . . . . . 14 |- (`'dom R C_ `'(dom C X. dom C) -> (`'(dom C X. dom C) C_ (dom C X. dom C) -> `'dom R C_ (dom C X. dom C)))
43		ssel 2615	. . . . . . . . . . . . . 14 |- (`'dom R C_ (dom C X. dom C) -> (<.x, y>. e. `'dom R -> <.x, y>. e. (dom C X. dom C)))
44	42, 43	syl6 25	. . . . . . . . . . . . 13 |- (`'dom R C_ `'(dom C X. dom C) -> (`'(dom C X. dom C) C_ (dom C X. dom C) -> (<.x, y>. e. `'dom R -> <.x, y>. e. (dom C X. dom C))))
45	41, 44	mpi 55	. . . . . . . . . . . 12 |- (`'dom R C_ `'(dom C X. dom C) -> (<.x, y>. e. `'dom R -> <.x, y>. e. (dom C X. dom C)))
46	40, 45	syl 12	. . . . . . . . . . 11 |- (dom R C_ (dom C X. dom C) -> (<.x, y>. e. `'dom R -> <.x, y>. e. (dom C X. dom C)))
47	46	3ad2ant2 898	. . . . . . . . . 10 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> (<.x, y>. e. `'dom R -> <.x, y>. e. (dom C X. dom C)))
48	47	anim1d 619	. . . . . . . . 9 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> ((<.x, y>. e. `'dom R /\ z = (yRx)) -> (<.x, y>. e. (dom C X. dom C) /\ z = (yRx))))
49	48	ssoprab2g 14333	. . . . . . . 8 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ {<.<.x, y>., z>. | (<.x, y>. e. (dom C X. dom C) /\ z = (yRx))})
50		oprex 4907	. . . . . . . . . . 11 |- (yRx) e. _V
51		twsvbdop 14332	. . . . . . . . . . 11 |- {<.<.x, y>., z>. | (<.x, y>. e. (dom C X. dom C) /\ z = (yRx))} = {<.<.x, y>., z>. | ((x e. dom C /\ y e. dom C) /\ z = (yRx))}
52	50, 51	fnoprab2 5064	. . . . . . . . . 10 |- {<.<.x, y>., z>. | (<.x, y>. e. (dom C X. dom C) /\ z = (yRx))} Fn (dom C X. dom C)
53		fnfun 4510	. . . . . . . . . 10 |- ({<.<.x, y>., z>. | (<.x, y>. e. (dom C X. dom C) /\ z = (yRx))} Fn (dom C X. dom C) -> Fun {<.<.x, y>., z>. | (<.x, y>. e. (dom C X. dom C) /\ z = (yRx))})
54	52, 53	ax-mp 7	. . . . . . . . 9 |- Fun {<.<.x, y>., z>. | (<.x, y>. e. (dom C X. dom C) /\ z = (yRx))}
55	54	a1i 8	. . . . . . . 8 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> Fun {<.<.x, y>., z>. | (<.x, y>. e. (dom C X. dom C) /\ z = (yRx))})
56		funss 4439	. . . . . . . 8 |- ({<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ {<.<.x, y>., z>. | (<.x, y>. e. (dom C X. dom C) /\ z = (yRx))} -> (Fun {<.<.x, y>., z>. | (<.x, y>. e. (dom C X. dom C) /\ z = (yRx))} -> Fun {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))}))
57	49, 55, 56	sylc 83	. . . . . . 7 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> Fun {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))})
58		relcnv 4301	. . . . . . . 8 |- Rel `'dom R
59		cnvxp 4332	. . . . . . . . . . . 12 |- `'(dom C X. dom C) = (dom C X. dom C)
60		sseq2 2639	. . . . . . . . . . . . 13 |- (`'(dom C X. dom C) = (dom C X. dom C) -> (`'dom R C_ `'(dom C X. dom C) <-> `'dom R C_ (dom C X. dom C)))
61		sseq1 2637	. . . . . . . . . . . . . . . 16 |- (`'dom R = dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} -> (`'dom R C_ (dom C X. dom C) <-> dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C)))
62	61	biimpd 170	. . . . . . . . . . . . . . 15 |- (`'dom R = dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} -> (`'dom R C_ (dom C X. dom C) -> dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C)))
63	62	eqcoms 1887	. . . . . . . . . . . . . 14 |- (dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} = `'dom R -> (`'dom R C_ (dom C X. dom C) -> dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C)))
64	63	com12 14	. . . . . . . . . . . . 13 |- (`'dom R C_ (dom C X. dom C) -> (dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} = `'dom R -> dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C)))
65	60, 64	syl6bi 231	. . . . . . . . . . . 12 |- (`'(dom C X. dom C) = (dom C X. dom C) -> (`'dom R C_ `'(dom C X. dom C) -> (dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} = `'dom R -> dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C))))
66	59, 65	ax-mp 7	. . . . . . . . . . 11 |- (`'dom R C_ `'(dom C X. dom C) -> (dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} = `'dom R -> dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C)))
67	40, 66	syl 12	. . . . . . . . . 10 |- (dom R C_ (dom C X. dom C) -> (dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} = `'dom R -> dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C)))
68	67	3ad2ant2 898	. . . . . . . . 9 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> (dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} = `'dom R -> dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C)))
69	50	dmoprabss6 14336	. . . . . . . . 9 |- (Rel `'dom R -> dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} = `'dom R)
70	68, 69	syl5com 63	. . . . . . . 8 |- (Rel `'dom R -> ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C)))
71	58, 70	ax-mp 7	. . . . . . 7 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C))
72		elrel 4086	. . . . . . . . . . . . . . . . . . 19 |- ((Rel `'dom R /\ w e. `'dom R) -> E.xE.y w = <.x, y>.)
73	1, 2	opelcnv 4143	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<.x, y>. e. `'dom R <-> <.y, x>. e. dom R)
74	1, 2	opswap 4374	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- U.`'{<.x, y>.} = <.y, x>.
75		simp1 876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((Fun R /\ U.`'{<.x, y>.} = <.y, x>. /\ <.y, x>. e. dom R) -> Fun R)
76		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (<.y, x>. = U.`'{<.x, y>.} -> (<.y, x>. e. dom R <-> U.`'{<.x, y>.} e. dom R))
77	76	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (<.y, x>. = U.`'{<.x, y>.} -> (<.y, x>. e. dom R -> U.`'{<.x, y>.} e. dom R))
78	77	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (U.`'{<.x, y>.} = <.y, x>. -> (<.y, x>. e. dom R -> U.`'{<.x, y>.} e. dom R))
79	78	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((U.`'{<.x, y>.} = <.y, x>. /\ <.y, x>. e. dom R) -> U.`'{<.x, y>.} e. dom R)
80	79	3adant1 894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((Fun R /\ U.`'{<.x, y>.} = <.y, x>. /\ <.y, x>. e. dom R) -> U.`'{<.x, y>.} e. dom R)
81		fvelrn 4785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((Fun R /\ U.`'{<.x, y>.} e. dom R) -> (R` U.`'{<.x, y>.}) e. ran R)
82	75, 80, 81	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((Fun R /\ U.`'{<.x, y>.} = <.y, x>. /\ <.y, x>. e. dom R) -> (R` U.`'{<.x, y>.}) e. ran R)
83	82	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (Fun R -> (U.`'{<.x, y>.} = <.y, x>. -> (<.y, x>. e. dom R -> (R` U.`'{<.x, y>.}) e. ran R)))
84	83	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (dom R C_ (dom C X. dom C) -> (Fun R -> (U.`'{<.x, y>.} = <.y, x>. -> (<.y, x>. e. dom R -> (R` U.`'{<.x, y>.}) e. ran R))))
85	84	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<.y, x>. e. dom R -> (Fun R -> (U.`'{<.x, y>.} = <.y, x>. -> (dom R C_ (dom C X. dom C) -> (R` U.`'{<.x, y>.}) e. ran R))))
86	85	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (ran R C_ dom C -> (<.y, x>. e. dom R -> (Fun R -> (U.`'{<.x, y>.} = <.y, x>. -> (dom R C_ (dom C X. dom C) -> (R` U.`'{<.x, y>.}) e. ran R)))))
87	86	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (U.`'{<.x, y>.} = <.y, x>. -> (<.y, x>. e. dom R -> (Fun R -> (ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{<.x, y>.}) e. ran R)))))
88	74, 87	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (<.y, x>. e. dom R -> (Fun R -> (ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{<.x, y>.}) e. ran R))))
89	88	a1d 15	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<.y, x>. e. dom R -> (w = <.x, y>. -> (Fun R -> (ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{<.x, y>.}) e. ran R)))))
90	73, 89	sylbi 216	. . . . . . . . . . . . . . . . . . . . . 22 |- (<.x, y>. e. `'dom R -> (w = <.x, y>. -> (Fun R -> (ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{<.x, y>.}) e. ran R)))))
91	90	com12 14	. . . . . . . . . . . . . . . . . . . . 21 |- (w = <.x, y>. -> (<.x, y>. e. `'dom R -> (Fun R -> (ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{<.x, y>.}) e. ran R)))))
92		eleq1 1957	. . . . . . . . . . . . . . . . . . . . 21 |- (w = <.x, y>. -> (w e. `'dom R <-> <.x, y>. e. `'dom R))
93		sneq 3054	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w = <.x, y>. -> {w} = {<.x, y>.})
94		cnveq 4135	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ({w} = {<.x, y>.} -> `'{w} = `'{<.x, y>.})
95	93, 94	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = <.x, y>. -> `'{w} = `'{<.x, y>.})
96	95	unieqd 3188	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = <.x, y>. -> U.`'{w} = U.`'{<.x, y>.})
97	96	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = <.x, y>. -> (R` U.`'{w}) = (R` U.`'{<.x, y>.}))
98	97	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = <.x, y>. -> ((R` U.`'{w}) e. ran R <-> (R` U.`'{<.x, y>.}) e. ran R))
99	98	imbi2d 674	. . . . . . . . . . . . . . . . . . . . . . 23 |- (w = <.x, y>. -> ((dom R C_ (dom C X. dom C) -> (R` U.`'{w}) e. ran R) <-> (dom R C_ (dom C X. dom C) -> (R` U.`'{<.x, y>.}) e. ran R)))
100	99	imbi2d 674	. . . . . . . . . . . . . . . . . . . . . 22 |- (w = <.x, y>. -> ((ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{w}) e. ran R)) <-> (ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{<.x, y>.}) e. ran R))))
101	100	imbi2d 674	. . . . . . . . . . . . . . . . . . . . 21 |- (w = <.x, y>. -> ((Fun R -> (ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{w}) e. ran R))) <-> (Fun R -> (ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{<.x, y>.}) e. ran R)))))
102	91, 92, 101	3imtr4d 602	. . . . . . . . . . . . . . . . . . . 20 |- (w = <.x, y>. -> (w e. `'dom R -> (Fun R -> (ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{w}) e. ran R)))))
103	102	19.23aivv 1675	. . . . . . . . . . . . . . . . . . 19 |- (E.xE.y w = <.x, y>. -> (w e. `'dom R -> (Fun R -> (ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{w}) e. ran R)))))
104	72, 103	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((Rel `'dom R /\ w e. `'dom R) -> (w e. `'dom R -> (Fun R -> (ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{w}) e. ran R)))))
105	104	ex 402	. . . . . . . . . . . . . . . . 17 |- (Rel `'dom R -> (w e. `'dom R -> (w e. `'dom R -> (Fun R -> (ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{w}) e. ran R))))))
106	105	pm2.43d 79	. . . . . . . . . . . . . . . 16 |- (Rel `'dom R -> (w e. `'dom R -> (Fun R -> (ran R C_ dom C -> (dom R C_ (dom C X. dom C) -> (R` U.`'{w}) e. ran R)))))
107	106	com25 48	. . . . . . . . . . . . . . 15 |- (Rel `'dom R -> (dom R C_ (dom C X. dom C) -> (Fun R -> (ran R C_ dom C -> (w e. `'dom R -> (R` U.`'{w}) e. ran R)))))
108	58, 107	ax-mp 7	. . . . . . . . . . . . . 14 |- (dom R C_ (dom C X. dom C) -> (Fun R -> (ran R C_ dom C -> (w e. `'dom R -> (R` U.`'{w}) e. ran R))))
109	108	com12 14	. . . . . . . . . . . . 13 |- (Fun R -> (dom R C_ (dom C X. dom C) -> (ran R C_ dom C -> (w e. `'dom R -> (R` U.`'{w}) e. ran R))))
110	109	3imp 1061	. . . . . . . . . . . 12 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> (w e. `'dom R -> (R` U.`'{w}) e. ran R))
111	110	r19.21aiv 2175	. . . . . . . . . . 11 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> A.w e. `' dom R(R` U.`'{w}) e. ran R)
112		eqid 1884	. . . . . . . . . . . 12 |- {<.w, z>. | (w e. `'dom R /\ z = (R` U.`'{w}))} = {<.w, z>. | (w e. `'dom R /\ z = (R` U.`'{w}))}
113	112	fopab2 4796	. . . . . . . . . . 11 |- (A.w e. `' dom R(R` U.`'{w}) e. ran R <-> {<.w, z>. | (w e. `'dom R /\ z = (R` U.`'{w}))}:`'dom R-->ran R)
114	111, 113	sylib 215	. . . . . . . . . 10 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> {<.w, z>. | (w e. `'dom R /\ z = (R` U.`'{w}))}:`'dom R-->ran R)
115		frn 4569	. . . . . . . . . 10 |- ({<.w, z>. | (w e. `'dom R /\ z = (R` U.`'{w}))}:`'dom R-->ran R -> ran {<.w, z>. | (w e. `'dom R /\ z = (R` U.`'{w}))} C_ ran R)
116	114, 115	syl 12	. . . . . . . . 9 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> ran {<.w, z>. | (w e. `'dom R /\ z = (R` U.`'{w}))} C_ ran R)
117		simp3 878	. . . . . . . . 9 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> ran R C_ dom C)
118	116, 117	sstrd 2627	. . . . . . . 8 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> ran {<.w, z>. | (w e. `'dom R /\ z = (R` U.`'{w}))} C_ dom C)
119		sneq 3054	. . . . . . . . . . . . . . . . 17 |- (<.x, y>. = w -> {<.x, y>.} = {w})
120		cnveq 4135	. . . . . . . . . . . . . . . . 17 |- ({<.x, y>.} = {w} -> `'{<.x, y>.} = `'{w})
121	119, 120	syl 12	. . . . . . . . . . . . . . . 16 |- (<.x, y>. = w -> `'{<.x, y>.} = `'{w})
122	121	unieqd 3188	. . . . . . . . . . . . . . 15 |- (<.x, y>. = w -> U.`'{<.x, y>.} = U.`'{w})
123	122	fveq2d 4685	. . . . . . . . . . . . . 14 |- (<.x, y>. = w -> (R` U.`'{<.x, y>.}) = (R` U.`'{w}))
124	74	eqcomi 1888	. . . . . . . . . . . . . . 15 |- <.y, x>. = U.`'{<.x, y>.}
125	124	fveq2i 4684	. . . . . . . . . . . . . 14 |- (R` <.y, x>.) = (R` U.`'{<.x, y>.})
126	123, 125	syl5eq 1940	. . . . . . . . . . . . 13 |- (<.x, y>. = w -> (R` <.y, x>.) = (R` U.`'{w}))
127	126	eqeq2d 1895	. . . . . . . . . . . 12 |- (<.x, y>. = w -> (z = (R` <.y, x>.) <-> z = (R` U.`'{w})))
128		df-opr 4886	. . . . . . . . . . . . 13 |- (yRx) = (R` <.y, x>.)
129	128	eqeq2i 1894	. . . . . . . . . . . 12 |- (z = (yRx) <-> z = (R` <.y, x>.))
130	127, 129	syl5bb 591	. . . . . . . . . . 11 |- (<.x, y>. = w -> (z = (yRx) <-> z = (R` U.`'{w})))
131	130	dfoprab4spop 14339	. . . . . . . . . 10 |- (Rel `'dom R -> {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} = {<.w, z>. | (w e. `'dom R /\ z = (R` U.`'{w}))})
132	58, 131	ax-mp 7	. . . . . . . . 9 |- {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} = {<.w, z>. | (w e. `'dom R /\ z = (R` U.`'{w}))}
133	132	rneqi 4187	. . . . . . . 8 |- ran {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} = ran {<.w, z>. | (w e. `'dom R /\ z = (R` U.`'{w}))}
134	118, 133	syl5ss 2661	. . . . . . 7 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> ran {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ dom C)
135	57, 71, 134	3jca 1050	. . . . . 6 |- ((Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C) -> (Fun {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} /\ dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C) /\ ran {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ dom C))
136	39, 135	anim12i 360	. . . . 5 |- (((D:dom C-->dom J /\ C:dom C-->dom J /\ J:dom J-->dom C) /\ (Fun R /\ dom R C_ (dom C X. dom C) /\ ran R C_ dom C)) -> ((C:dom C-->dom J /\ D:dom C-->dom J /\ J:dom J-->dom C) /\ (Fun {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} /\ dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C) /\ ran {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ dom C)))
137	35, 136	syl6 25	. . . 4 |- (dom D = dom C -> (((D:dom D-->dom J /\ C:dom D-->dom J /\ J:dom J-->dom D) /\ (Fun R /\ dom R C_ (dom D X. dom D) /\ ran R C_ dom D)) -> ((C:dom C-->dom J /\ D:dom C-->dom J /\ J:dom J-->dom C) /\ (Fun {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} /\ dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C) /\ ran {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ dom C))))
138	13, 18, 137	sylc 83	. . 3 |- (T e. Alg -> ((C:dom C-->dom J /\ D:dom C-->dom J /\ J:dom J-->dom C) /\ (Fun {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} /\ dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C) /\ ran {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ dom C)))
139		fvex 4689	. . . . . . . 8 |- (cod` T) e. _V
140	12, 139	eqeltri 1967	. . . . . . 7 |- C e. _V
141		fvex 4689	. . . . . . . 8 |- (dom` T) e. _V
142	11, 141	eqeltri 1967	. . . . . . 7 |- D e. _V
143		fvex 4689	. . . . . . . 8 |- (id` T) e. _V
144	14, 143	eqeltri 1967	. . . . . . 7 |- J e. _V
145	140, 142, 144	3pm3.2i 1048	. . . . . 6 |- (C e. _V /\ D e. _V /\ J e. _V)
146		fvex 4689	. . . . . . . . . 10 |- (o` T) e. _V
147	15, 146	eqeltri 1967	. . . . . . . . 9 |- R e. _V
148	147	dmex 4208	. . . . . . . 8 |- dom R e. _V
149	148	cnvex 4425	. . . . . . 7 |- `'dom R e. _V
150		oprabex2gpop 14337	. . . . . . 7 |- ((`'dom R e. _V /\ Rel `'dom R) -> {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} e. _V)
151	149, 58, 150	mp2an 761	. . . . . 6 |- {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} e. _V
152	145, 151	pm3.2i 307	. . . . 5 |- ((C e. _V /\ D e. _V /\ J e. _V) /\ {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} e. _V)
153	152	a1i 8	. . . 4 |- (T e. Alg -> ((C e. _V /\ D e. _V /\ J e. _V) /\ {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} e. _V))
154		eqid 1884	. . . . 5 |- dom C = dom C
155	154, 17	isalg 15068	. . . 4 |- (((C e. _V /\ D e. _V /\ J e. _V) /\ {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} e. _V) -> (<.<.C, D>., <.J, {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))}>.>. e. Alg <-> ((C:dom C-->dom J /\ D:dom C-->dom J /\ J:dom J-->dom C) /\ (Fun {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} /\ dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C) /\ ran {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ dom C))))
156	153, 155	syl 12	. . 3 |- (T e. Alg -> (<.<.C, D>., <.J, {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))}>.>. e. Alg <-> ((C:dom C-->dom J /\ D:dom C-->dom J /\ J:dom J-->dom C) /\ (Fun {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} /\ dom {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ (dom C X. dom C) /\ ran {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))} C_ dom C))))
157	138, 156	mpbird 213	. 2 |- (T e. Alg -> <.<.C, D>., <.J, {<.<.x, y>., z>. | (<.x, y>. e. `'dom R /\ z = (yRx))}>.>. e. Alg )
158	10, 157	eqeltrd 1971	1 |- (T e. Alg -> <.<.C, D>., <.J, {<.<.x, y>., z>. | (<.y, x>. e. dom R /\ z = (yRx))}>.>. e. Alg )

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  _Vcvv 2292   C_ wss 2593  {csn 3044  <.cop 3046  U.cuni 3177  {copab 3395   X. cxp 3984  `'ccnv 3985  dom cdm 3986  ran crn 3987  Rel wrel 3991  Fun wfun 3992   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  {copab2 4885   Alg calg 15058  domcdom_ 15059  codccod_ 15060  idcid_ 15061  oco_ 15062

This theorem is referenced by:  dualded 15132

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-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

Copyright terms: Public domain