Theorem algi 10660

Description: Properties of an the structure of Alg and Ded.

Hypotheses

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

Assertion

Ref	Expression
algi	|- (T e. Alg -> ((D:M-->O /\ C:M-->O /\ J:O-->M) /\ (Fun R /\ dom R (_ (M X. M) /\ ran R (_ M)))

Proof of Theorem algi

Step	Hyp	Ref	Expression
1		df-alg 10648	. . 3 |- Alg = {x | E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ (d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d))}
2	1	eleq2i 1538	. 2 |- (T e. Alg <-> T e. {x | E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ (d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d))})
3		3anass 779	. . . . . . . 8 |- ((x = <.<.d, c>., <.j, r>.>. /\ (d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d)) <-> (x = <.<.d, c>., <.j, r>.>. /\ ((d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d))))
4	3	bicomi 172	. . . . . . 7 |- ((x = <.<.d, c>., <.j, r>.>. /\ ((d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d))) <-> (x = <.<.d, c>., <.j, r>.>. /\ (d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d)))
5	4	exbii 1051	. . . . . 6 |- (E.r(x = <.<.d, c>., <.j, r>.>. /\ ((d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d))) <-> E.r(x = <.<.d, c>., <.j, r>.>. /\ (d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d)))
6	5	3exbi 1053	. . . . 5 |- (E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ ((d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d))) <-> E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ (d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d)))
7	6	abbii 1575	. . . 4 |- {x | E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ ((d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d)))} = {x | E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ (d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d))}
8	7	eleq2i 1538	. . 3 |- (T e. {x | E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ ((d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d)))} <-> T e. {x | E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ (d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d))})
9		algi.1	. . . . . . . 8 |- D = (dom` T)
10	9	domval 10655	. . . . . . 7 |- D = (1st` (1st` T))
11	10	eqcomi 1479	. . . . . 6 |- (1st` (1st` T)) = D
12	11	eqeq2i 1485	. . . . 5 |- (d = (1st` (1st` T)) <-> d = D)
13		feq1 3620	. . . . . . . 8 |- (d = D -> (d:dom d-->dom j <-> D:dom d-->dom j))
14		dmeq 3311	. . . . . . . . . 10 |- (d = D -> dom d = dom D)
15		feq2 3621	. . . . . . . . . 10 |- (dom d = dom D -> (D:dom d-->dom j <-> D:dom D-->dom j))
16	14, 15	syl 10	. . . . . . . . 9 |- (d = D -> (D:dom d-->dom j <-> D:dom D-->dom j))
17		algi.5	. . . . . . . . . 10 |- M = dom D
18		feq2 3621	. . . . . . . . . 10 |- (M = dom D -> (D:M-->dom j <-> D:dom D-->dom j))
19	17, 18	ax-mp 7	. . . . . . . . 9 |- (D:M-->dom j <-> D:dom D-->dom j)
20	16, 19	syl6bbr 538	. . . . . . . 8 |- (d = D -> (D:dom d-->dom j <-> D:M-->dom j))
21	13, 20	bitrd 528	. . . . . . 7 |- (d = D -> (d:dom d-->dom j <-> D:M-->dom j))
22		feq2 3621	. . . . . . . . 9 |- (dom d = dom D -> (c:dom d-->dom j <-> c:dom D-->dom j))
23		feq2 3621	. . . . . . . . . 10 |- (M = dom D -> (c:M-->dom j <-> c:dom D-->dom j))
24	17, 23	ax-mp 7	. . . . . . . . 9 |- (c:M-->dom j <-> c:dom D-->dom j)
25	22, 24	syl6bbr 538	. . . . . . . 8 |- (dom d = dom D -> (c:dom d-->dom j <-> c:M-->dom j))
26	14, 25	syl 10	. . . . . . 7 |- (d = D -> (c:dom d-->dom j <-> c:M-->dom j))
27	17	eqcomi 1479	. . . . . . . . . 10 |- dom D = M
28	27	eqeq2i 1485	. . . . . . . . 9 |- (dom d = dom D <-> dom d = M)
29	28	biimp 151	. . . . . . . 8 |- (dom d = dom D -> dom d = M)
30		feq3 3622	. . . . . . . 8 |- (dom d = M -> (j:dom j-->dom d <-> j:dom j-->M))
31	14, 29, 30	3syl 20	. . . . . . 7 |- (d = D -> (j:dom j-->dom d <-> j:dom j-->M))
32	21, 26, 31	3anbi123d 893	. . . . . 6 |- (d = D -> ((d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) <-> (D:M-->dom j /\ c:M-->dom j /\ j:dom j-->M)))
33		xpid11 3335	. . . . . . . . 9 |- ((dom d X. dom d) = (M X. M) <-> dom d = M)
34		sseq2 2083	. . . . . . . . 9 |- ((dom d X. dom d) = (M X. M) -> (dom r (_ (dom d X. dom d) <-> dom r (_ (M X. M)))
35	33, 34	sylbir 201	. . . . . . . 8 |- (dom d = M -> (dom r (_ (dom d X. dom d) <-> dom r (_ (M X. M)))
36		sseq2 2083	. . . . . . . 8 |- (dom d = M -> (ran r (_ dom d <-> ran r (_ M))
37	35, 36	3anbi23d 896	. . . . . . 7 |- (dom d = M -> ((Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d) <-> (Fun r /\ dom r (_ (M X. M) /\ ran r (_ M)))
38	14, 29, 37	3syl 20	. . . . . 6 |- (d = D -> ((Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d) <-> (Fun r /\ dom r (_ (M X. M) /\ ran r (_ M)))
39	32, 38	anbi12d 628	. . . . 5 |- (d = D -> (((d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d)) <-> ((D:M-->dom j /\ c:M-->dom j /\ j:dom j-->M) /\ (Fun r /\ dom r (_ (M X. M) /\ ran r (_ M))))
40	12, 39	sylbi 199	. . . 4 |- (d = (1st` (1st` T)) -> (((d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d)) <-> ((D:M-->dom j /\ c:M-->dom j /\ j:dom j-->M) /\ (Fun r /\ dom r (_ (M X. M) /\ ran r (_ M))))
41		algi.2	. . . . . . . 8 |- C = (cod` T)
42	41	codval&nb