Definition df-grp 9594

Description: Define class of all groups.

Assertion

Ref	Expression
df-grp	|- Grp = {f | E.gE.p(g = (Base` f) /\ p = (+g` f) /\ (A.a e. g A.b e. g A.c e. g ((apb) e. g /\ ((apb)pc) = (ap(bpc))) /\ E.e e. g A.a e. g ((epa) = a /\ E.m e. g (mpa) = e)))}

Distinct variable group:   a,b,c,e,f,g,m,p

Detailed syntax breakdown of Definition df-grp

Step	Hyp	Ref	Expression
1		cgrp 9581	. 2 class Grp
2		vg	. . . . . . . 8 set g
3	2	cv 1614	. . . . . . 7 class g
4		vf	. . . . . . . . 9 set f
5	4	cv 1614	. . . . . . . 8 class f
6		cbs 9579	. . . . . . . 8 class Base
7	5, 6	cfv 4163	. . . . . . 7 class (Base` f)
8	3, 7	wceq 1615	. . . . . 6 wff g = (Base` f)
9		vp	. . . . . . . 8 set p
10	9	cv 1614	. . . . . . 7 class p
11		cplusg 9580	. . . . . . . 8 class +g
12	5, 11	cfv 4163	. . . . . . 7 class (+g` f)
13	10, 12	wceq 1615	. . . . . 6 wff p = (+g` f)
14		va	. . . . . . . . . . . . . 14 set a
15	14	cv 1614	. . . . . . . . . . . . 13 class a
16		vb	. . . . . . . . . . . . . 14 set b
17	16	cv 1614	. . . . . . . . . . . . 13 class b
18	15, 17, 10	co 5020	. . . . . . . . . . . 12 class (apb)
19	18, 3	wcel 1617	. . . . . . . . . . 11 wff (apb) e. g
20		vc	. . . . . . . . . . . . . 14 set c
21	20	cv 1614	. . . . . . . . . . . . 13 class c
22	18, 21, 10	co 5020	. . . . . . . . . . . 12 class ((apb)pc)
23	17, 21, 10	co 5020	. . . . . . . . . . . . 13 class (bpc)
24	15, 23, 10	co 5020	. . . . . . . . . . . 12 class (ap(bpc))
25	22, 24	wceq 1615	. . . . . . . . . . 11 wff ((apb)pc) = (ap(bpc))
26	19, 25	wa 433	. . . . . . . . . 10 wff ((apb) e. g /\ ((apb)pc) = (ap(bpc)))
27	26, 20, 3	wral 2385	. . . . . . . . 9 wff A.c e. g ((apb) e. g /\ ((apb)pc) = (ap(bpc)))
28	27, 16, 3	wral 2385	. . . . . . . 8 wff A.b e. g A.c e. g ((apb) e. g /\ ((apb)pc) = (ap(bpc)))
29	28, 14, 3	wral 2385	. . . . . . 7 wff A.a e. g A.b e. g A.c e. g ((apb) e. g /\ ((apb)pc) = (ap(bpc)))
30		ve	. . . . . . . . . . . . 13 set e
31	30	cv 1614	. . . . . . . . . . . 12 class e
32	31, 15, 10	co 5020	. . . . . . . . . . 11 class (epa)
33	32, 15	wceq 1615	. . . . . . . . . 10 wff (epa) = a
34		vm	. . . . . . . . . . . . . 14 set m
35	34	cv 1614	. . . . . . . . . . . . 13 class m
36	35, 15, 10	co 5020	. . . . . . . . . . . 12 class (mpa)
37	36, 31	wceq 1615	. . . . . . . . . . 11 wff (mpa) = e
38	37, 34, 3	wrex 2386	. . . . . . . . . 10 wff E.m e. g (mpa) = e
39	33, 38	wa 433	. . . . . . . . 9 wff ((epa) = a /\ E.m e. g (mpa) = e)
40	39, 14, 3	wral 2385	. . . . . . . 8 wff A.a e. g ((epa) = a /\ E.m e. g (mpa) = e)
41	40, 30, 3	wrex 2386	. . . . . . 7 wff E.e e. g A.a e. g ((epa) = a /\ E.m e. g (mpa) = e)
42	29, 41	wa 433	. . . . . 6 wff (A.a e. g A.b e. g A.c e. g ((apb) e. g /\ ((apb)pc) = (ap(bpc))) /\ E.e e. g A.a e. g ((epa) = a /\ E.m e. g (mpa) = e))
43	8, 13, 42	w3a 1130	. . . . 5 wff (g = (Base` f) /\ p = (+g` f) /\ (A.a e. g A.b e. g A.c e. g ((apb) e. g /\ ((apb)pc) = (ap(bpc))) /\ E.e e. g A.a e. g ((epa) = a /\ E.m e. g (mpa) = e)))
44	43, 9	wex 1644	. . . 4 wff E.p(g = (Base` f) /\ p = (+g` f) /\ (A.a e. g A.b e. g A.c e. g ((apb) e. g /\ ((apb)pc) = (ap(bpc))) /\ E.e e. g A.a e. g ((epa) = a /\ E.m e. g (mpa) = e)))
45	44, 2	wex 1644	. . 3 wff E.gE.p(g = (Base` f) /\ p = (+g` f) /\ (A.a e. g A.b e. g A.c e. g ((apb) e. g /\ ((apb)pc) = (ap(bpc))) /\ E.e e. g A.a e. g ((epa) = a /\ E.m e. g (mpa) = e)))
46	45, 4	cab 2157	. 2 class {f | E.gE.p(g = (Base` f) /\ p = (+g` f) /\ (A.a e. g A.b e. g A.c e. g ((apb) e. g /\ ((apb)pc) = (ap(bpc))) /\ E.e e. g A.a e. g ((epa) = a /\ E.m e. g (mpa) = e)))}
47	1, 46	wceq 1615	1 wff Grp = {f | E.gE.p(g = (Base` f) /\ p = (+g` f) /\ (A.a e. g A.b e. g A.c e. g ((apb) e. g /\ ((apb)pc) = (ap(bpc))) /\ E.e e. g A.a e. g ((epa) = a /\ E.m e. g (mpa) = e)))}

This definition is referenced by:  isgrp 9611

Copyright terms: Public domain