Theorem dedi 15084

Description: Properties of a deductive system.

Hypotheses

Ref	Expression
dedi.1	|- D = (dom` T)
dedi.2	|- C = (cod` T)
dedi.3	|- J = (id` T)
dedi.4	|- R = (o` T)
dedi.5	|- M = dom D
dedi.6	|- O = dom J

Assertion

Ref	Expression
dedi	|- (T e. Ded -> ((<.<.D, C>., <.J, R>.>. e. Alg /\ A.a e. O ((D` (J` a)) = a /\ (C` (J` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom R <-> (D` g) = (C` f))) /\ (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (gRf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (gRf)) = (C` g)))))

Distinct variable groups:   C,a,f,g   D,a,f,g   J,a   R,f,g

Proof of Theorem dedi

Step	Hyp	Ref	Expression
1		df-ded 15082	. . 3 |- Ded = {x | E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ ((<.<.d, c>., <.j, r>.>. e. Alg /\ A.a e. dom j((d` (j` a)) = a /\ (c` (j` a)) = a) /\ A.f e. dom dA.g e. dom d(<.g, f>. e. dom r <-> (d` g) = (c` f))) /\ (A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (d` (grf)) = (d` f)) /\ A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (c` (grf)) = (c` g)))))}
2	1	eleq2i 1961	. 2 |- (T e. Ded <-> T e. {x | E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ ((<.<.d, c>., <.j, r>.>. e. Alg /\ A.a e. dom j((d` (j` a)) = a /\ (c` (j` a)) = a) /\ A.f e. dom dA.g e. dom d(<.g, f>. e. dom r <-> (d` g) = (c` f))) /\ (A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (d` (grf)) = (d` f)) /\ A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (c` (grf)) = (c` g)))))})
3		dedi.1	. . . . . . 7 |- D = (dom` T)
4	3	domval 15070	. . . . . 6 |- D = (1st` (1st` T))
5	4	eqcomi 1888	. . . . 5 |- (1st` (1st` T)) = D
6	5	eqeq2i 1894	. . . 4 |- (d = (1st` (1st` T)) <-> d = D)
7		opeq1 3158	. . . . . . . 8 |- (d = D -> <.d, c>. = <.D, c>.)
8	7	opeq1d 3164	. . . . . . 7 |- (d = D -> <.<.d, c>., <.j, r>.>. = <.<.D, c>., <.j, r>.>.)
9	8	eleq1d 1963	. . . . . 6 |- (d = D -> (<.<.d, c>., <.j, r>.>. e. Alg <-> <.<.D, c>., <.j, r>.>. e. Alg ))
10		fveq1 4680	. . . . . . . . 9 |- (d = D -> (d` (j` a)) = (D` (j` a)))
11	10	eqeq1d 1892	. . . . . . . 8 |- (d = D -> ((d` (j` a)) = a <-> (D` (j` a)) = a))
12	11	anbi1d 679	. . . . . . 7 |- (d = D -> (((d` (j` a)) = a /\ (c` (j` a)) = a) <-> ((D` (j` a)) = a /\ (c` (j` a)) = a)))
13	12	ralbidv 2123	. . . . . 6 |- (d = D -> (A.a e. dom j((d` (j` a)) = a /\ (c` (j` a)) = a) <-> A.a e. dom j((D` (j` a)) = a /\ (c` (j` a)) = a)))
14		dmeq 4157	. . . . . . . . . 10 |- (d = D -> dom d = dom D)
15		dedi.5	. . . . . . . . . 10 |- M = dom D
16	14, 15	syl6eqr 1946	. . . . . . . . 9 |- (d = D -> dom d = M)
17	16	eleq2d 1964	. . . . . . . 8 |- (d = D -> (f e. dom d <-> f e. M))
18	16	eleq2d 1964	. . . . . . . . . 10 |- (d = D -> (g e. dom d <-> g e. M))
19		fveq1 4680	. . . . . . . . . . . 12 |- (d = D -> (d` g) = (D` g))
20	19	eqeq1d 1892	. . . . . . . . . . 11 |- (d = D -> ((d` g) = (c` f) <-> (D` g) = (c` f)))
21	20	bibi2d 680	. . . . . . . . . 10 |- (d = D -> ((<.g, f>. e. dom r <-> (d` g) = (c` f)) <-> (<.g, f>. e. dom r <-> (D` g) = (c` f))))
22	18, 21	imbi12d 688	. . . . . . . . 9 |- (d = D -> ((g e. dom d -> (<.g, f>. e. dom r <-> (d` g) = (c` f))) <-> (g e. M -> (<.g, f>. e. dom r <-> (D` g) = (c` f)))))
23	22	ralbidv2 2125	. . . . . . . 8 |- (d = D -> (A.g e. dom d(<.g, f>. e. dom r <-> (d` g) = (c` f)) <-> A.g e. M (<.g, f>. e. dom r <-> (D` g) = (c` f))))
24	17, 23	imbi12d 688	. . . . . . 7 |- (d = D -> ((f e. dom d -> A.g e. dom d(<.g, f>. e. dom r <-> (d` g) = (c` f))) <-> (f e. M -> A.g e. M (<.g, f>. e. dom r <-> (D` g) = (c` f)))))
25	24	ralbidv2 2125	. . . . . 6 |- (d = D -> (A.f e. dom dA.g e. dom d(<.g, f>. e. dom r <-> (d` g) = (c` f)) <-> A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (c` f))))
26	9, 13, 25	3anbi123d 1168	. . . . 5 |- (d = D -> ((<.<.d, c>., <.j, r>.>. e. Alg /\ A.a e. dom j((d` (j` a)) = a /\ (c` (j` a)) = a) /\ A.f e. dom dA.g e. dom d(<.g, f>. e. dom r <-> (d` g) = (c` f))) <-> (<.<.D, c>., <.j, r>.>. e. Alg /\ A.a e. dom j((D` (j` a)) = a /\ (c` (j` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (c` f)))))
27		fveq1 4680	. . . . . . . . . . . 12 |- (d = D -> (d` (grf)) = (D` (grf)))
28		fveq1 4680	. . . . . . . . . . . 12 |- (d = D -> (d` f) = (D` f))
29	27, 28	eqeq12d 1899	. . . . . . . . . . 11 |- (d = D -> ((d` (grf)) = (d` f) <-> (D` (grf)) = (D` f)))
30	20, 29	imbi12d 688	. . . . . . . . . 10 |- (d = D -> (((d` g) = (c` f) -> (d` (grf)) = (d` f)) <-> ((D` g) = (c` f) -> (D` (grf)) = (D` f))))
31	18, 30	imbi12d 688	. . . . . . . . 9 |- (d = D -> ((g e. dom d -> ((d` g) = (c` f) -> (d` (grf)) = (d` f))) <-> (g e. M -> ((D` g) = (c` f) -> (D` (grf)) = (D` f)))))
32	31	ralbidv2 2125	. . . . . . . 8 |- (d = D -> (A.g e. dom d((d` g) = (c` f) -> (d` (grf)) = (d` f)) <-> A.g e. M ((D` g) = (c` f) -> (D` (grf)) = (D` f))))
33	17, 32	imbi12d 688	. . . . . . 7 |- (d = D -> ((f e. dom d -> A.g e. dom d((d` g) = (c` f) -> (d` (grf)) = (d` f))) <-> (f e. M -> A.g e. M ((D` g) = (c` f) -> (D` (grf)) = (D` f)))))
34	33	ralbidv2 2125	. . . . . 6 |- (d = D -> (A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (d` (grf)) = (d` f)) <-> A.f e. M A.g e. M ((D` g) = (c` f) -> (D` (grf)) = (D` f))))
35	20	imbi1d 675	. . . . . . . . . 10 |- (d = D -> (((d` g) = (c` f) -> (c` (grf)) = (c` g)) <-> ((D` g) = (c` f) -> (c` (grf)) = (c` g))))
36	18, 35	imbi12d 688	. . . . . . . . 9 |- (d = D -> ((g e. dom d -> ((d` g) = (c` f) -> (c` (grf)) = (c` g))) <-> (g e. M -> ((D` g) = (c` f) -> (c` (grf)) = (c` g)))))
37	36	ralbidv2 2125	. . . . . . . 8 |- (d = D -> (A.g e. dom d((d` g) = (c` f) -> (c` (grf)) = (c` g)) <-> A.g e. M ((D` g) = (c` f) -> (c` (grf)) = (c` g))))
38	17, 37	imbi12d 688	. . . . . . 7 |- (d = D -> ((f e. dom d -> A.g e. dom d((d` g) = (c` f) -> (c` (grf)) = (c` g))) <-> (f e. M -> A.g e. M ((D` g) = (c` f) -> (c` (grf)) = (c` g)))))
39	38	ralbidv2 2125	. . . . . 6 |- (d = D -> (A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (c` (grf)) = (c` g)) <-> A.f e. M A.g e. M ((D` g) = (c` f) -> (c` (grf)) = (c` g))))
40	34, 39	anbi12d 690	. . . . 5 |- (d = D -> ((A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (d` (grf)) = (d` f)) /\ A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (c` (grf)) = (c` g))) <-> (A.f e. M A.g e. M ((D` g) = (c` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (c` f) -> (c` (grf)) = (c` g)))))
41	26, 40	anbi12d 690	. . . 4 |- (d = D -> (((<.<.d, c>., <.j, r>.>. e. Alg /\ A.a e. dom j((d` (j` a)) = a /\ (c` (j` a)) = a) /\ A.f e. dom dA.g e. dom d(<.g, f>. e. dom r <-> (d` g) = (c` f))) /\ (A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (d` (grf)) = (d` f)) /\ A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (c` (grf)) = (c` g)))) <-> ((<.<.D, c>., <.j, r>.>. e. Alg /\ A.a e. dom j((D` (j` a)) = a /\ (c` (j` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (c` f))) /\ (A.f e. M A.g e. M ((D` g) = (c` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (c` f) -> (c` (grf)) = (c` g))))))
42	6, 41	sylbi 216	. . 3 |- (d = (1st` (1st` T)) -> (((<.<.d, c>., <.j, r>.>. e. Alg /\ A.a e. dom j((d` (j` a)) = a /\ (c` (j` a)) = a) /\ A.f e. dom dA.g e. dom d(<.g, f>. e. dom r <-> (d` g) = (c` f))) /\ (A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (d` (grf)) = (d` f)) /\ A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (c` (grf)) = (c` g)))) <-> ((<.<.D, c>., <.j, r>.>. e. Alg /\ A.a e. dom j((D` (j` a)) = a /\ (c` (j` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (c` f))) /\ (A.f e. M A.g e. M ((D` g) = (c` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (c` f) -> (c` (grf)) = (c` g))))))
43		dedi.2	. . . . . . 7 |- C = (cod` T)
44	43	codval 15071	. . . . . 6 |- C = (2nd` (1st` T))
45	44	eqcomi 1888	. . . . 5 |- (2nd` (1st` T)) = C
46	45	eqeq2i 1894	. . . 4 |- (c = (2nd` (1st` T)) <-> c = C)
47		opeq2 3159	. . . . . . . 8 |- (c = C -> <.D, c>. = <.D, C>.)
48	47	opeq1d 3164	. . . . . . 7 |- (c = C -> <.<.D, c>., <.j, r>.>. = <.<.D, C>., <.j, r>.>.)
49	48	eleq1d 1963	. . . . . 6 |- (c = C -> (<.<.D, c>., <.j, r>.>. e. Alg <-> <.<.D, C>., <.j, r>.>. e. Alg ))
50		fveq1 4680	. . . . . . . . 9 |- (c = C -> (c` (j` a)) = (C` (j` a)))
51	50	eqeq1d 1892	. . . . . . . 8 |- (c = C -> ((c` (j` a)) = a <-> (C` (j` a)) = a))
52	51	anbi2d 678	. . . . . . 7 |- (c = C -> (((D` (j` a)) = a /\ (c` (j` a)) = a) <-> ((D` (j` a)) = a /\ (C` (j` a)) = a)))
53	52	ralbidv 2123	. . . . . 6 |- (c = C -> (A.a e. dom j((D` (j` a)) = a /\ (c` (j` a)) = a) <-> A.a e. dom j((D` (j` a)) = a /\ (C` (j` a)) = a)))
54		fveq1 4680	. . . . . . . . 9 |- (c = C -> (c` f) = (C` f))
55	54	eqeq2d 1895	. . . . . . . 8 |- (c = C -> ((D` g) = (c` f) <-> (D` g) = (C` f)))
56	55	bibi2d 680	. . . . . . 7 |- (c = C -> ((<.g, f>. e. dom r <-> (D` g) = (c` f)) <-> (<.g, f>. e. dom r <-> (D` g) = (C` f))))
57	56	2ralbidv 2140	. . . . . 6 |- (c = C -> (A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (c` f)) <-> A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f))))
58	49, 53, 57	3anbi123d 1168	. . . . 5 |- (c = C -> ((<.<.D, c>., <.j, r>.>. e. Alg /\ A.a e. dom j((D` (j` a)) = a /\ (c` (j` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (c` f))) <-> (<.<.D, C>., <.j, r>.>. e. Alg /\ A.a e. dom j((D` (j` a)) = a /\ (C` (j` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f)))))
59	55	imbi1d 675	. . . . . . 7 |- (c = C -> (((D` g) = (c` f) -> (D` (grf)) = (D` f)) <-> ((D` g) = (C` f) -> (D` (grf)) = (D` f))))
60	59	2ralbidv 2140	. . . . . 6 |- (c = C -> (A.f e. M A.g e. M ((D` g) = (c` f) -> (D` (grf)) = (D` f)) <-> A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (grf)) = (D` f))))
61		fveq1 4680	. . . . . . . . 9 |- (c = C -> (c` (grf)) = (C` (grf)))
62		fveq1 4680	. . . . . . . . 9 |- (c = C -> (c` g) = (C` g))
63	61, 62	eqeq12d 1899	. . . . . . . 8 |- (c = C -> ((c` (grf)) = (c` g) <-> (C` (grf)) = (C` g)))
64	55, 63	imbi12d 688	. . . . . . 7 |- (c = C -> (((D` g) = (c` f) -> (c` (grf)) = (c` g)) <-> ((D` g) = (C` f) -> (C` (grf)) = (C` g))))
65	64	2ralbidv 2140	. . . . . 6 |- (c = C -> (A.f e. M A.g e. M ((D` g) = (c` f) -> (c` (grf)) = (c` g)) <-> A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (grf)) = (C` g))))
66	60, 65	anbi12d 690	. . . . 5 |- (c = C -> ((A.f e. M A.g e. M ((D` g) = (c` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (c` f) -> (c` (grf)) = (c` g))) <-> (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (grf)) = (C` g)))))
67	58, 66	anbi12d 690	. . . 4 |- (c = C -> (((<.<.D, c>., <.j, r>.>. e. Alg /\ A.a e. dom j((D` (j` a)) = a /\ (c` (j` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (c` f))) /\ (A.f e. M A.g e. M ((D` g) = (c` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (c` f) -> (c` (grf)) = (c` g)))) <-> ((<.<.D, C>., <.j, r>.>. e. Alg /\ A.a e. dom j((D` (j` a)) = a /\ (C` (j` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f))) /\ (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (grf)) = (C` g))))))
68	46, 67	sylbi 216	. . 3 |- (c = (2nd` (1st` T)) -> (((<.<.D, c>., <.j, r>.>. e. Alg /\ A.a e. dom j((D` (j` a)) = a /\ (c` (j` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (c` f))) /\ (A.f e. M A.g e. M ((D` g) = (c` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (c` f) -> (c` (grf)) = (c` g)))) <-> ((<.<.D, C>., <.j, r>.>. e. Alg /\ A.a e. dom j((D` (j` a)) = a /\ (C` (j` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f))) /\ (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (grf)) = (C` g))))))
69		dedi.3	. . . . . . 7 |- J = (id` T)
70	69	idval 15072	. . . . . 6 |- J = (1st` (2nd` T))
71	70	eqcomi 1888	. . . . 5 |- (1st` (2nd` T)) = J
72	71	eqeq2i 1894	. . . 4 |- (j = (1st` (2nd` T)) <-> j = J)
73		opeq1 3158	. . . . . . . 8 |- (j = J -> <.j, r>. = <.J, r>.)
74	73	opeq2d 3165	. . . . . . 7 |- (j = J -> <.<.D, C>., <.j, r>.>. = <.<.D, C>., <.J, r>.>.)
75	74	eleq1d 1963	. . . . . 6 |- (j = J -> (<.<.D, C>., <.j, r>.>. e. Alg <-> <.<.D, C>., <.J, r>.>. e. Alg ))
76		dmeq 4157	. . . . . . . . . 10 |- (j = J -> dom j = dom J)
77		dedi.6	. . . . . . . . . 10 |- O = dom J
78	76, 77	syl6eqr 1946	. . . . . . . . 9 |- (j = J -> dom j = O)
79	78	eleq2d 1964	. . . . . . . 8 |- (j = J -> (a e. dom j <-> a e. O))
80		fveq1 4680	. . . . . . . . . . 11 |- (j = J -> (j` a) = (J` a))
81	80	fveq2d 4685	. . . . . . . . . 10 |- (j = J -> (D` (j` a)) = (D` (J` a)))
82	81	eqeq1d 1892	. . . . . . . . 9 |- (j = J -> ((D` (j` a)) = a <-> (D` (J` a)) = a))
83	80	fveq2d 4685	. . . . . . . . . 10 |- (j = J -> (C` (j` a)) = (C` (J` a)))
84	83	eqeq1d 1892	. . . . . . . . 9 |- (j = J -> ((C` (j` a)) = a <-> (C` (J` a)) = a))
85	82, 84	anbi12d 690	. . . . . . . 8 |- (j = J -> (((D` (j` a)) = a /\ (C` (j` a)) = a) <-> ((D` (J` a)) = a /\ (C` (J` a)) = a)))
86	79, 85	imbi12d 688	. . . . . . 7 |- (j = J -> ((a e. dom j -> ((D` (j` a)) = a /\ (C` (j` a)) = a)) <-> (a e. O -> ((D` (J` a)) = a /\ (C` (J` a)) = a))))
87	86	ralbidv2 2125	. . . . . 6 |- (j = J -> (A.a e. dom j((D` (j` a)) = a /\ (C` (j` a)) = a) <-> A.a e. O ((D` (J` a)) = a /\ (C` (J` a)) = a)))
88	75, 87	3anbi12d 1169	. . . . 5 |- (j = J -> ((<.<.D, C>., <.j, r>.>. e. Alg /\ A.a e. dom j((D` (j` a)) = a /\ (C` (j` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f))) <-> (<.<.D, C>., <.J, r>.>. e. Alg /\ A.a e. O ((D` (J` a)) = a /\ (C` (J` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f)))))
89	88	anbi1d 679	. . . 4 |- (j = J -> (((<.<.D, C>., <.j, r>.>. e. Alg /\ A.a e. dom j((D` (j` a)) = a /\ (C` (j` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f))) /\ (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (grf)) = (C` g)))) <-> ((<.<.D, C>., <.J, r>.>. e. Alg /\ A.a e. O ((D` (J` a)) = a /\ (C` (J` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f))) /\ (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (grf)) = (C` g))))))
90	72, 89	sylbi 216	. . 3 |- (j = (1st` (2nd` T)) -> (((<.<.D, C>., <.j, r>.>. e. Alg /\ A.a e. dom j((D` (j` a)) = a /\ (C` (j` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f))) /\ (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (grf)) = (C` g)))) <-> ((<.<.D, C>., <.J, r>.>. e. Alg /\ A.a e. O ((D` (J` a)) = a /\ (C` (J` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f))) /\ (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (grf)) = (C` g))))))
91		dedi.4	. . . . . . 7 |- R = (o` T)
92	91	cmpval 15073	. . . . . 6 |- R = (2nd` (2nd` T))
93	92	eqcomi 1888	. . . . 5 |- (2nd` (2nd` T)) = R
94	93	eqeq2i 1894	. . . 4 |- (r = (2nd` (2nd` T)) <-> r = R)
95		opeq2 3159	. . . . . . . 8 |- (r = R -> <.J, r>. = <.J, R>.)
96	95	opeq2d 3165	. . . . . . 7 |- (r = R -> <.<.D, C>., <.J, r>.>. = <.<.D, C>., <.J, R>.>.)
97	96	eleq1d 1963	. . . . . 6 |- (r = R -> (<.<.D, C>., <.J, r>.>. e. Alg <-> <.<.D, C>., <.J, R>.>. e. Alg ))
98		dmeq 4157	. . . . . . . . 9 |- (r = R -> dom r = dom R)
99	98	eleq2d 1964	. . . . . . . 8 |- (r = R -> (<.g, f>. e. dom r <-> <.g, f>. e. dom R))
100	99	bibi1d 681	. . . . . . 7 |- (r = R -> ((<.g, f>. e. dom r <-> (D` g) = (C` f)) <-> (<.g, f>. e. dom R <-> (D` g) = (C` f))))
101	100	2ralbidv 2140	. . . . . 6 |- (r = R -> (A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f)) <-> A.f e. M A.g e. M (<.g, f>. e. dom R <-> (D` g) = (C` f))))
102	97, 101	3anbi13d 1170	. . . . 5 |- (r = R -> ((<.<.D, C>., <.J, r>.>. e. Alg /\ A.a e. O ((D` (J` a)) = a /\ (C` (J` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f))) <-> (<.<.D, C>., <.J, R>.>. e. Alg /\ A.a e. O ((D` (J` a)) = a /\ (C` (J` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom R <-> (D` g) = (C` f)))))
103		opreq 4888	. . . . . . . . . 10 |- (r = R -> (grf) = (gRf))
104	103	fveq2d 4685	. . . . . . . . 9 |- (r = R -> (D` (grf)) = (D` (gRf)))
105	104	eqeq1d 1892	. . . . . . . 8 |- (r = R -> ((D` (grf)) = (D` f) <-> (D` (gRf)) = (D` f)))
106	105	imbi2d 674	. . . . . . 7 |- (r = R -> (((D` g) = (C` f) -> (D` (grf)) = (D` f)) <-> ((D` g) = (C` f) -> (D` (gRf)) = (D` f))))
107	106	2ralbidv 2140	. . . . . 6 |- (r = R -> (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (grf)) = (D` f)) <-> A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (gRf)) = (D` f))))
108	103	fveq2d 4685	. . . . . . . . 9 |- (r = R -> (C` (grf)) = (C` (gRf)))
109	108	eqeq1d 1892	. . . . . . . 8 |- (r = R -> ((C` (grf)) = (C` g) <-> (C` (gRf)) = (C` g)))
110	109	imbi2d 674	. . . . . . 7 |- (r = R -> (((D` g) = (C` f) -> (C` (grf)) = (C` g)) <-> ((D` g) = (C` f) -> (C` (gRf)) = (C` g))))
111	110	2ralbidv 2140	. . . . . 6 |- (r = R -> (A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (grf)) = (C` g)) <-> A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (gRf)) = (C` g))))
112	107, 111	anbi12d 690	. . . . 5 |- (r = R -> ((A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (grf)) = (C` g))) <-> (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (gRf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (gRf)) = (C` g)))))
113	102, 112	anbi12d 690	. . . 4 |- (r = R -> (((<.<.D, C>., <.J, r>.>. e. Alg /\ A.a e. O ((D` (J` a)) = a /\ (C` (J` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f))) /\ (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (grf)) = (C` g)))) <-> ((<.<.D, C>., <.J, R>.>. e. Alg /\ A.a e. O ((D` (J` a)) = a /\ (C` (J` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom R <-> (D` g) = (C` f))) /\ (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (gRf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (gRf)) = (C` g))))))
114	94, 113	sylbi 216	. . 3 |- (r = (2nd` (2nd` T)) -> (((<.<.D, C>., <.J, r>.>. e. Alg /\ A.a e. O ((D` (J` a)) = a /\ (C` (J` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom r <-> (D` g) = (C` f))) /\ (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (grf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (grf)) = (C` g)))) <-> ((<.<.D, C>., <.J, R>.>. e. Alg /\ A.a e. O ((D` (J` a)) = a /\ (C` (J` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom R <-> (D` g) = (C` f))) /\ (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (gRf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (gRf)) = (C` g))))))
115	42, 68, 90, 114	eloi 14400	. 2 |- (T e. {x | E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ ((<.<.d, c>., <.j, r>.>. e. Alg /\ A.a e. dom j((d` (j` a)) = a /\ (c` (j` a)) = a) /\ A.f e. dom dA.g e. dom d(<.g, f>. e. dom r <-> (d` g) = (c` f))) /\ (A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (d` (grf)) = (d` f)) /\ A.f e. dom dA.g e. dom d((d` g) = (c` f) -> (c` (grf)) = (c` g)))))} -> ((<.<.D, C>., <.J, R>.>. e. Alg /\ A.a e. O ((D` (J` a)) = a /\ (C` (J` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom R <-> (D` g) = (C` f))) /\ (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (gRf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (gRf)) = (C` g)))))
116	2, 115	sylbi 216	1 |- (T e. Ded -> ((<.<.D, C>., <.J, R>.>. e. Alg /\ A.a e. O ((D` (J` a)) = a /\ (C` (J` a)) = a) /\ A.f e. M A.g e. M (<.g, f>. e. dom R <-> (D` g) = (C` f))) /\ (A.f e. M A.g e. M ((D` g) = (C` f) -> (D` (gRf)) = (D` f)) /\ A.f e. M A.g e. M ((D` g) = (C` f) -> (C` (gRf)) = (C` g)))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  A.wral 2105  <.cop 3046  dom cdm 3986  ` cfv 3998  (class class class)co 4884  1stc1st 5018  2ndc2nd 5019   Alg calg 15058  domcdom_ 15059  codccod_ 15060  idcid_ 15061  oco_ 15062   Ded cded 15081

This theorem is referenced by:  dedalg 15090  idosd 15091  cmppfd 15092  domcmpd 15093  codcmpd 15094

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-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-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-1st 5020  df-2nd 5021  df-doma 15064  df-coda 15065  df-ida 15066  df-cmpa 15067  df-ded 15082

Copyright terms: Public domain