Theorem dedi 10621

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 10619	. . 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 1537	. 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 10606	. . . . . 6 |- D = (1st` (1st` T))
5	4	eqcomi 1478	. . . . 5 |- (1st` (1st` T)) = D
6	5	eqeq2i 1484	. . . 4 |- (d = (1st` (1st` T)) <-> d = D)
7		opeq1 2485	. . . . . . . 8 |- (d = D -> <.d, c>. = <.D, c>.)
8	7	opeq1d 2491	. . . . . . 7 |- (d = D -> <.<.d, c>., <.j, r>.>. = <.<.D, c>., <.j, r>.>.)
9	8	eleq1d 1539	. . . . . 6 |- (d = D -> (<.<.d, c>., <.j, r>.>. e. Alg <-> <.<.D, c>., <.j, r>.>. e. Alg))
10		fveq1 3720	. . . . . . . . 9 |- (d = D -> (d` (j` a)) = (D` (j` a)))
11	10	eqeq1d 1482	. . . . . . . 8 |- (d = D -> ((d` (j` a)) = a <-> (D` (j` a)) = a))
12	11	anbi1d 616	. . . . . . 7 |- (d = D -> (((d` (j` a)) = a /\ (c` (j` a)) = a) <-> ((D` (j` a)) = a /\ (c` (j` a)) = a)))
13	12	ralbidv 1662	. . . . . 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 3308	. . . . . . . . . 10 |- (d = D -> dom d = dom D)
15		dedi.5	. . . . . . . . . 10 |- M = dom D
16	14, 15	syl6eqr 1524	. . . . . . . . 9 |- (d = D -> dom d = M)
17	16	eleq2d 1540	. . . . . . . 8 |- (d = D -> (f e. dom d <-> f e. M))
18	16	eleq2d 1540	. . . . . . . . . 10 |- (d = D -> (g e. dom d <-> g e. M))
19		fveq1 3720	. . . . . . . . . . . 12 |- (d = D -> (d` g) = (D` g))
20	19	eqeq1d 1482	. . . . . . . . . . 11 |- (d = D -> ((d` g) = (c` f) <-> (D` g) = (c` f)))
21	20	bibi2d 617	. . . . . . . . . 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 625	. . . . . . . . 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 1664	. . . . . . . 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 625	. . . . . . 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 1664	. . . . . 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 892	. . . . 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 3720	. . . . . . . . . . . 12 |- (d = D -> (d` (grf)) = (D` (grf)))
28		fveq1 3720	. . . . . . . . . . . 12 |- (d = D -> (d` f) = (D` f))
29	27, 28	eqeq12d 1488	. . . . . . . . . . 11 |- (d = D -> ((d` (grf)) = (d` f) <-> (D` (grf)) = (D` f)))
30	20, 29	imbi12d 625	. . . . . . . . . 10 |- (d = D -> (((d` g) = (c` f) -> (d` (grf)) = (d` f)) <-> ((D` g) = (c` f) -> (D` (grf)) = (D` f))))
31	18, 30	imbi12d 625	. . . . . . . . 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 1664	. . . . . . . 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 625	. . . . . . 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 1664	. . . . . 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 612	. . . . . . . . . 10 |- (d = D -> (((d` g) = (c` f) -> (c` (grf)) = (c` g)) <-> ((D` g) = (c` f) -> (c` (grf)) = (c` g))))
36	18, 35	imbi12d