Theorem isalg 15068

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

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 C_ (M X. M) /\ ran R C_ M))))

Proof of Theorem isalg

Step	Hyp	Ref	Expression
1		feq1 4551	. . . . . . 7 |- (d = D -> (d:dom d-->dom j <-> D:dom d-->dom j))
2		dmeq 4157	. . . . . . . 8 |- (d = D -> dom d = dom D)
3		isalg.1	. . . . . . . . . . 11 |- M = dom D
4	3	eqcomi 1888	. . . . . . . . . 10 |- dom D = M
5	4	eqeq2i 1894	. . . . . . . . 9 |- (dom d = dom D <-> dom d = M)
6	5	biimpi 168	. . . . . . . 8 |- (dom d = dom D -> dom d = M)
7		feq2 4552	. . . . . . . 8 |- (dom d = M -> (D:dom d-->dom j <-> D:M-->dom j))
8	2, 6, 7	3syl 24	. . . . . . 7 |- (d = D -> (D:dom d-->dom j <-> D:M-->dom j))
9	1, 8	bitrd 587	. . . . . 6 |- (d = D -> (d:dom d-->dom j <-> D:M-->dom j))
10		feq2 4552	. . . . . . 7 |- (dom d = M -> (c:dom d-->dom j <-> c:M-->dom j))
11	2, 6, 10	3syl 24	. . . . . 6 |- (d = D -> (c:dom d-->dom j <-> c:M-->dom j))
12		feq3 4553	. . . . . . 7 |- (dom d = M -> (j:dom j-->dom d <-> j:dom j-->M))
13	2, 6, 12	3syl 24	. . . . . 6 |- (d = D -> (j:dom j-->dom d <-> j:dom j-->M))
14	9, 11, 13	3anbi123d 1168	. . . . 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 1946	. . . . . . 7 |- (d = D -> dom d = M)
16		xpid11 4181	. . . . . . . 8 |- ((dom d X. dom d) = (M X. M) <-> dom d = M)
17	16	biimpri 169	. . . . . . 7 |- (dom d = M -> (dom d X. dom d) = (M X. M))
18		sseq2 2639	. . . . . . 7 |- ((dom d X. dom d) = (M X. M) -> (dom r C_ (dom d X. dom d) <-> dom r C_ (M X. M)))
19	15, 17, 18	3syl 24	. . . . . 6 |- (d = D -> (dom r C_ (dom d X. dom d) <-> dom r C_ (M X. M)))
20		sseq2 2639	. . . . . . 7 |- (dom d = M -> (ran r C_ dom d <-> ran r C_ M))
21	2, 6, 20	3syl 24	. . . . . 6 |- (d = D -> (ran r C_ dom d <-> ran r C_ M))
22	19, 21	3anbi23d 1171	. . . . 5 |- (d = D -> ((Fun r /\ dom r C_ (dom d X. dom d) /\ ran r C_ dom d) <-> (Fun r /\ dom r C_ (M X. M) /\ ran r C_ M)))
23	14, 22	anbi12d 690	. . . 4 |- (d = D -> (((d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r C_ (dom d X. dom d) /\ ran r C_ dom d)) <-> ((D:M-->dom j /\ c:M-->dom j /\ j:dom j-->M) /\ (Fun r /\ dom r C_ (M X. M) /\ ran r C_ M))))
24		feq1 4551	. . . . . 6 |- (c = C -> (c:M-->dom j <-> C:M-->dom j))
25	24	3anbi2d 1173	. . . . 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 679	. . . 4 |- (c = C -> (((D:M-->dom j /\ c:M-->dom j /\ j:dom j-->M) /\ (Fun r /\ dom r C_ (M X. M) /\ ran r C_ M)) <-> ((D:M-->dom j /\ C:M-->dom j /\ j:dom j-->M) /\ (Fun r /\ dom r C_ (M X. M) /\ ran r C_ M))))
27		dmeq 4157	. . . . . . 7 |- (j = J -> dom j = dom J)
28		isalg.2	. . . . . . . . . 10 |- O = dom J
29	28	eqcomi 1888	. . . . . . . . 9 |- dom J = O
30	29	eqeq2i 1894	. . . . . . . 8 |- (dom j = dom J <-> dom j = O)
31	30	biimpi 168	. . . . . . 7 |- (dom j = dom J -> dom j = O)
32		feq3 4553	. . . . . . 7 |- (dom j = O -> (D:M-->dom j <-> D:M-->O))
33	27, 31, 32	3syl 24	. . . . . 6 |- (j = J -> (D:M-->dom j <-> D:M-->O))
34		feq3 4553	. . . . . . 7 |- (dom j = O -> (C:M-->dom j <-> C:M-->O))
35	27, 31, 34	3syl 24	. . . . . 6 |- (j = J -> (C:M-->dom j <-> C:M-->O))
36		feq1 4551	. . . . . . 7 |- (j = J -> (j:dom j-->M <-> J:dom j-->M))
37		feq2 4552	. . . . . . . 8 |- (dom j = O -> (J:dom j-->M <-> J:O-->M))
38	27, 31, 37	3syl 24	. . . . . . 7 |- (j = J -> (J:dom j-->M <-> J:O-->M))
39	36, 38	bitrd 587	. . . . . 6 |- (j = J -> (j:dom j-->M <-> J:O-->M))
40	33, 35, 39	3anbi123d 1168	. . . . 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 679	. . . 4 |- (j = J -> (((D:M-->dom j /\ C:M-->dom j /\ j:dom j-->M) /\ (Fun r /\ dom r C_ (M X. M) /\ ran r C_ M)) <-> ((D:M-->O /\ C:M-->O /\ J:O-->M) /\ (Fun r /\ dom r C_ (M X. M) /\ ran r C_ M))))
42		funeq 4441	. . . . . 6 |- (r = R -> (Fun r <-> Fun R))
43		dmeq 4157	. . . . . . 7 |- (r = R -> dom r = dom R)
44	43	sseq1d 2644	. . . . . 6 |- (r = R -> (dom r C_ (M X. M) <-> dom R C_ (M X. M)))
45		rneq 4186	. . . . . . 7 |- (r = R -> ran r = ran R)
46	45	sseq1d 2644	. . . . . 6 |- (r = R -> (ran r C_ M <-> ran R C_ M))
47	42, 44, 46	3anbi123d 1168	. . . . 5 |- (r = R -> ((Fun r /\ dom r C_ (M X. M) /\ ran r C_ M) <-> (Fun R /\ dom R C_ (M X. M) /\ ran R C_ M)))
48	47	anbi2d 678	. . . 4 |- (r = R -> (((D:M-->O /\ C:M-->O /\ J:O-->M) /\ (Fun r /\ dom r C_ (M X. M) /\ ran r C_ M)) <-> ((D:M-->O /\ C:M-->O /\ J:O-->M) /\ (Fun R /\ dom R C_ (M X. M) /\ ran R C_ M))))
49	23, 26, 41, 48	elo 14342	. . 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 C_ (dom d X. dom d) /\ ran r C_ dom d)))} <-> ((D:M-->O /\ C:M-->O /\ J:O-->M) /\ (Fun R /\ dom R C_ (M X. M) /\ ran R C_ M))))
50		3anass 862	. . . . . . 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 C_ (dom d X. dom d) /\ ran r C_ 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 C_ (dom d X. dom d) /\ ran r C_ dom d))))
51	50	exbii 1398	. . . . . 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 C_ (dom d X. dom d) /\ ran r C_ 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 C_ (dom d X. dom d) /\ ran r C_ dom d))))
52	51	3exbii 1400	. . . . 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 C_ (dom d X. dom d) /\ ran r C_ 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 C_ (dom d X. dom d) /\ ran r C_ dom d))))
53	52	abbii 2006	. . . 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 C_ (dom d X. dom d) /\ ran r C_ 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 C_ (dom d X. dom d) /\ ran r C_ dom d)))}
54	53	eleq2i 1961	. . 3 |- (<.<.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 C_ (dom d X. dom d) /\ ran r C_ dom d))} <-> <.<.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 C_ (dom d X. dom d) /\ ran r C_ dom d)))})
55	49, 54	syl5bb 591	. 2 |- (((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 C_ (dom d X. dom d) /\ ran r C_ dom d))} <-> ((D:M-->O /\ C:M-->O /\ J:O-->M) /\ (Fun R /\ dom R C_ (M X. M) /\ ran R C_ M))))
56		df-alg 15063	. . 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 C_ (dom d X. dom d) /\ ran r C_ dom d))}
57	56	eleq2i 1961	. 2 |- (<.<.D, C>., <.J, R>.>. e. Alg <-> <.<.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 C_ (dom d X. dom d) /\ ran r C_ dom d))})
58	55, 57	syl5bb 591	1 |- (((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 C_ (M X. M) /\ ran R C_ M))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871   C_ wss 2593  <.cop 3046   X. cxp 3984  dom cdm 3986  ran crn 3987  Fun wfun 3992  -->wf 3994   Alg calg 15058

This theorem is referenced by:  1alg 15069  0alg 15103  dualalg 15131

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-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

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-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-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-fun 4008  df-fn 4009  df-f 4010  df-alg 15063

Copyright terms: Public domain