Theorem isded 10640

Description: The predicate "is a deductive system".

Hypotheses

Ref	Expression
isded.1	|- M = dom D
isded.2	|- O = dom J

Assertion

Ref	Expression
isded	|- (((D e. A /\ C e. B /\ J e. F) /\ R e. G) -> (<.<.D, C>., <.J, R>.>. 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 isded

Step	Hyp	Ref	Expression
1		opeq1 2491	. . . . . . 7 |- (d = D -> <.d, c>. = <.D, c>.)
2	1	opeq1d 2497	. . . . . 6 |- (d = D -> <.<.d, c>., <.j, r>.>. = <.<.D, c>., <.j, r>.>.)
3	2	eleq1d 1543	. . . . 5 |- (d = D -> (<.<.d, c>., <.j, r>.>. e. Alg <-> <.<.D, c>., <.j, r>.>. e. Alg))
4		fveq1 3729	. . . . . . . 8 |- (d = D -> (d` (j` a)) = (D` (j` a)))
5	4	eqeq1d 1486	. . . . . . 7 |- (d = D -> ((d` (j` a)) = a <-> (D` (j` a)) = a))
6	5	anbi1d 619	. . . . . 6 |- (d = D -> (((d` (j` a)) = a /\ (c` (j` a)) = a) <-> ((D` (j` a)) = a /\ (c` (j` a)) = a)))
7	6	ralbidv 1666	. . . . 5 |- (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)))
8		dmeq 3317	. . . . . . . . 9 |- (d = D -> dom d = dom D)
9		isded.1	. . . . . . . . 9 |- M = dom D
10	8, 9	syl6eqr 1528	. . . . . . . 8 |- (d = D -> dom d = M)
11	10	eleq2d 1544	. . . . . . 7 |- (d = D -> (f e. dom d <-> f e. M))
12	10	eleq2d 1544	. . . . . . . . 9 |- (d = D -> (g e. dom d <-> g e. M))
13		fveq1 3729	. . . . . . . . . . 11 |- (d = D -> (d` g) = (D` g))
14	13	eqeq1d 1486	. . . . . . . . . 10 |- (d = D -> ((d` g) = (c` f) <-> (D` g) = (c` f)))
15	14	bibi2d 620	. . . . . . . . 9 |- (d = D -> ((<.g, f>. e. dom r <-> (d` g) = (c` f)) <-> (<.g, f>. e. dom r <-> (D` g) = (c` f))))
16	12, 15	imbi12d 628	. . . . . . . 8 |- (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)))))
17	16	ralbidv2 1668	. . . . . . 7 |- (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))))
18	11, 17	imbi12d 628	. . . . . 6 |- (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)))))
19	18	ralbidv2 1668	. . . . 5 |- (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))))
20	3, 7, 19	3anbi123d 895	. . . 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))) <-> (<.<.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)))))
21		fveq1 3729	. . . . . . . . . . 11 |- (d = D -> (d` (grf)) = (D` (grf)))
22		fveq1 3729	. . . . . . . . . . 11 |- (d = D -> (d` f) = (D` f))
23	21, 22	eqeq12d 1492	. . . . . . . . . 10 |- (d = D -> ((d` (grf)) = (d` f) <-> (D` (grf)) = (D` f)))
24	14, 23	imbi12d 628	. . . . . . . . 9 |- (d = D -> (((d` g) = (c` f) -> (d` (grf)) = (d` f)) <-> ((D` g) = (c` f) -> (D` (grf)) = (D` f))))
25	12, 24	imbi12d 628	. . . . . . . 8 |- (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)))))
26	25	ralbidv2 1668	. . . . . . 7 |- (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))))
27	11, 26	imbi12d 628	. . . . . 6 |- (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)))))
28	27	ralbidv2 1668	. . . . 5 |- (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))))
29	14	imbi1d 615	. . . . . . . . 9 |- (d = D -> (((d` g) = (c` f) -> (c` (grf)) = (c` g)) <-> ((D` g) = (c` f) -> (c` (grf)) = (c` g))))
30	12, 29	imbi12d 628	. . . . . . . 8 |- (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)))))
31	30	ralbidv2 1668	. . . . . . 7 |- (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))))
32	11, 31	imbi12d 628	. . . . . 6 |- (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)))))
33	32	ralbidv2 1668	. . . . 5 |- (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))))
34	28, 33	anbi12d 630	. . . 4 |- (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))