Theorem isalg 10653

Description: The predicate "has the structure required by Alg and Ded."

Hypotheses

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

Assertion

Ref	Expression
isalg	|- (((D e. A /\ C e. B /\ J e. F) /\ R e. G) -> (<.<.D, C>., <.J, R>.>. e. Alg <-> ((D:M-->O /\ C:M-->O /\ J:O-->M) /\ (Fun R /\ dom R (_ (M X. M) /\ ran R (_ M))))

Proof of Theorem isalg

Step	Hyp	Ref	Expression
1		feq1 3620	. . . . . . 7 |- (d = D -> (d:dom d-->dom j <-> D:dom d-->dom j))
2		dmeq 3311	. . . . . . . 8 |- (d = D -> dom d = dom D)
3		isalg.1	. . . . . . . . . . 11 |- M = dom D
4	3	eqcomi 1479	. . . . . . . . . 10 |- dom D = M
5	4	eqeq2i 1485	. . . . . . . . 9 |- (dom d = dom D <-> dom d = M)
6	5	biimp 151	. . . . . . . 8 |- (dom d = dom D -> dom d = M)
7		feq2 3621	. . . . . . . 8 |- (dom d = M -> (D:dom d-->dom j <-> D:M-->dom j))
8	2, 6, 7	3syl 20	. . . . . . 7 |- (d = D -> (D:dom d-->dom j <-> D:M-->dom j))
9	1, 8	bitrd 528	. . . . . 6 |- (d = D -> (d:dom d-->dom j <-> D:M-->dom j))
10		feq2 3621	. . . . . . 7 |- (dom d = M -> (c:dom d-->dom j <-> c:M-->dom j))
11	2, 6, 10	3syl 20	. . . . . 6 |- (d = D -> (c:dom d-->dom j <-> c:M-->dom j))
12		feq3 3622	. . . . . . 7 |- (dom d = M -> (j:dom j-->dom d <-> j:dom j-->M))
13	2, 6, 12	3syl 20	. . . . . 6 |- (d = D -> (j:dom j-->dom d <-> j:dom j-->M))
14	9, 11, 13	3anbi123d 893	. . . . 5 |- (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)))
15	2, 3	syl6eqr 1525	. . . . . . 7 |- (d = D -> dom d = M)
16		xpid11 3335	. . . . . . . 8 |- ((dom d X. dom d) = (M X. M) <-> dom d = M)
17	16	biimpr 152	. . . . . . 7 |- (dom d = M -> (dom d X. dom d) = (M X. M))
18		sseq2 2083	. . . . . . 7 |- ((dom d X. dom d) = (M X. M) -> (dom r (_ (dom d X. dom d) <-> dom r (_ (M X. M)))
19	15, 17, 18	3syl 20	. . . . . 6 |- (d = D -> (dom r (_ (dom d X. dom d) <-> dom r (_ (M X. M)))
20		sseq2 2083	. . . . . . 7 |- (dom d = M -> (ran r (_ dom d <-> ran r (_ M))
21	2, 6, 20	3syl 20	. . . . . 6 |- (d = D -> (ran r (_ dom d <-> ran r (_ M))
22	19, 21	3anbi23d 896	. . . . 5 |- (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)))
23	14, 22	anbi12d 628	. . . 4 |- (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))))
24		feq1 3620	. . . . . 6 |- (c = C -> (c:M-->dom j <-> C:M-->dom j))
25	24	3anbi2d 898	. . . . 5 |- (c = C -> ((D:M-->dom j /\ c:M-->dom j /\ j:dom j-->M) <-> (D:M-->dom j /\ C:M-->dom j /\ j:dom j-->M)))
26	25	anbi1d 617	. . . 4 |- (c = C -> (((D:M-->dom j /\ c:M-->dom j /\ j:dom j-->M) /\ (Fun r /\ dom r (_ (M X. M) /\ ran r (_ M)) <-> ((D:M-->dom j /\ C:M-->dom j /\ j:dom j-->M) /\ (Fun r /\ dom r (_ (M X. M) /\ ran r (_ M))))
27		dmeq 3311	. . . . . . 7 |- (j = J -> dom j = dom J)
28		isalg.2	. . . . . . . . . 10 |- O = dom J
29	28	eqcomi 1479	. . . . . . . . 9 |- dom J = O
30	29	eqeq2i 1485	. . . . . . . 8 |- (dom j = dom J <-> dom j = O)
31	30	biimp 151	. . . . . . 7 |- (dom j = dom J -> dom j = O)
32		feq3 3622	. . . . . . 7 |- (dom j = O -> (D:M-->dom j <-> D:M-->O))
33	27, 31, 32	3syl 20	. . . . . 6 |- (j = J -> (D:M-->dom j <-> D:M-->O))
34		feq3 3622	. . . . . . 7 |- (dom j = O -> (C:M-->dom j <-> C:M-->O))
35	27, 31, 34	3syl 20	. . . . . 6 |- (j = J -> (C:M-->dom j <-> C:M-->O))
36		feq1 3620	. . . . . . 7 |- (j = J -> (j:dom j-->M <-> J:dom j-->M))
37		feq2 3621	. . . . . . . 8 |- (dom j = O -> (J:dom j-->M <-> J:O-->M))
38	27, 31, 37	3syl 20	. . . . . . 7 |- (j = J -> (J:dom j-->M <-> J:O-->M))
39	36, 38	bitrd 528	. . . . . 6 |- (j = J -> (j:dom j-->M <-> J:O-->M))
40	33, 35, 39	3anbi123d 893	. . . . 5 |- (j = J -> ((D:M-->dom j /\ C:M-->dom j /\ j:dom j-->M) <-> (D:M-->O /\ C:M-->O /\ J:O-->M)))
41	40	anbi1d 617	. . . 4 |- (j = J -> (((D:M-->dom j /\ C:M-->dom j /\ j:dom j-->M) /\ (Fun r /\ dom r (_ (M X. M) /\ ran r (_ M)) <-> ((D:M-->O /\ C:M-->O /\ J:O-->M) /\ (Fun r /\ dom r (_ (M X. M) /\ ran r (_ M))))
42		funeq 3535	. . . . . 6 |- (r = R -> (Fun r <-> Fun R))
43		dmeq 3311	. . . . . . 7 |- (r = R -> dom r = dom R)
44	43	sseq1d 2088	. . . . . 6 |- (r = R -> (dom r (_ (M X. M) <-> dom R (_ (M X. M)))
45		rneq 3339	. . . . . . 7 |- (r = R -> ran r = ran R)
46	45	sseq1d 2088	. . . . . 6 |- (r = R -> (ran r (_ M <-> ran R (_ M))
47	42, 44, 46	3anbi123d 893	. . . . 5 |- (r = R -> ((Fun r /\ dom r (_ (M X. M) /\ ran r (_ M) <-> (Fun R /\ dom R (_ (M X. M) /\ ran R (_ M)))
48	47	anbi2d 616	. . . 4 |- (r = R -> (((D:M-->O /\ C:M-->O /\ J:O-->M) /\ (Fun r /\ dom r (_ (M X. M) /\ ran r (_ M)) <-> ((D:M-->O /\ C:M-->O /\ J:O-->M) /\ (Fun R /\ dom R (_ (M X. M) /\ ran R (_ M))))
49	23, 26, 41, 48	elo 10444	. . 3 |- (((D e. A /\ C e. B /\ J e. F) /\ R e. G) -> (<.<.D, C>., <.J, R>.>. 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)))} <-> ((D:M-->O /\ C:M-->O /\ J:O-->M) /\ (Fun R /\ dom R (_ (M X. M) /\ ran R (_ M))))
50		3anass 779	. . . . . . 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))))
51	50	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))))
52	51	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