Definition df-cgr3 24073

Description: The three place congruence predicate. This is an abbreviation for saying that all three pair in a triple are congruent with each other. Three place form of Definition 4.4 of [Schwabhauser] p. 35. (Contributed by Scott Fenton, 4-Oct-2013.)

Assertion

Ref	Expression
df-cgr3	|- Cgr3 = { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. e e. ( EE ` n ) E. f e. ( EE ` n ) ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ( <. a , b >.Cgr <. d , e >. /\ <. a , c >.Cgr <. d , f >. /\ <. b , c >.Cgr <. e , f >. ) ) }

Distinct variable group:   a, b, c, d, e, f, n, p, q

Detailed syntax breakdown of Definition df-cgr3

Step	Hyp	Ref	Expression
1		ccgr3 24069	. 2 class Cgr3
2		vp	. . . . . . . . . . . . 13 set p
3	2	cv 1622	. . . . . . . . . . . 12 class p
4		va	. . . . . . . . . . . . . 14 set a
5	4	cv 1622	. . . . . . . . . . . . 13 class a
6		vb	. . . . . . . . . . . . . . 15 set b
7	6	cv 1622	. . . . . . . . . . . . . 14 class b
8		vc	. . . . . . . . . . . . . . 15 set c
9	8	cv 1622	. . . . . . . . . . . . . 14 class c
10	7, 9	cop 3644	. . . . . . . . . . . . 13 class <. b , c >.
11	5, 10	cop 3644	. . . . . . . . . . . 12 class <. a , <. b , c >. >.
12	3, 11	wceq 1623	. . . . . . . . . . 11 wff p = <. a , <. b , c >. >.
13		vq	. . . . . . . . . . . . 13 set q
14	13	cv 1622	. . . . . . . . . . . 12 class q
15		vd	. . . . . . . . . . . . . 14 set d
16	15	cv 1622	. . . . . . . . . . . . 13 class d
17		ve	. . . . . . . . . . . . . . 15 set e
18	17	cv 1622	. . . . . . . . . . . . . 14 class e
19		vf	. . . . . . . . . . . . . . 15 set f
20	19	cv 1622	. . . . . . . . . . . . . 14 class f
21	18, 20	cop 3644	. . . . . . . . . . . . 13 class <. e , f >.
22	16, 21	cop 3644	. . . . . . . . . . . 12 class <. d , <. e , f >. >.
23	14, 22	wceq 1623	. . . . . . . . . . 11 wff q = <. d , <. e , f >. >.
24	5, 7	cop 3644	. . . . . . . . . . . . 13 class <. a , b >.
25	16, 18	cop 3644	. . . . . . . . . . . . 13 class <. d , e >.
26		ccgr 23928	. . . . . . . . . . . . 13 class Cgr
27	24, 25, 26	wbr 4024	. . . . . . . . . . . 12 wff <. a , b >.Cgr <. d , e >.
28	5, 9	cop 3644	. . . . . . . . . . . . 13 class <. a , c >.
29	16, 20	cop 3644	. . . . . . . . . . . . 13 class <. d , f >.
30	28, 29, 26	wbr 4024	. . . . . . . . . . . 12 wff <. a , c >.Cgr <. d , f >.
31	10, 21, 26	wbr 4024	. . . . . . . . . . . 12 wff <. b , c >.Cgr <. e , f >.
32	27, 30, 31	w3a 934	. . . . . . . . . . 11 wff ( <. a , b >.Cgr <. d , e >. /\ <. a , c >.Cgr <. d , f >. /\ <. b , c >.Cgr <. e , f >. )
33	12, 23, 32	w3a 934	. . . . . . . . . 10 wff ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ( <. a , b >.Cgr <. d , e >. /\ <. a , c >.Cgr <. d , f >. /\ <. b , c >.Cgr <. e , f >. ) )
34		vn	. . . . . . . . . . . 12 set n
35	34	cv 1622	. . . . . . . . . . 11 class n
36		cee 23926	. . . . . . . . . . 11 class EE
37	35, 36	cfv 5221	. . . . . . . . . 10 class ( EE ` n )
38	33, 19, 37	wrex 2545	. . . . . . . . 9 wff E. f e. ( EE ` n ) ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ( <. a , b >.Cgr <. d , e >. /\ <. a , c >.Cgr <. d , f >. /\ <. b , c >.Cgr <. e , f >. ) )
39	38, 17, 37	wrex 2545	. . . . . . . 8 wff E. e e. ( EE ` n ) E. f e. ( EE ` n ) ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ( <. a , b >.Cgr <. d , e >. /\ <. a , c >.Cgr <. d , f >. /\ <. b , c >.Cgr <. e , f >. ) )
40	39, 15, 37	wrex 2545	. . . . . . 7 wff E. d e. ( EE ` n ) E. e e. ( EE ` n ) E. f e. ( EE ` n ) ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ( <. a , b >.Cgr <. d , e >. /\ <. a , c >.Cgr <. d , f >. /\ <. b , c >.Cgr <. e , f >. ) )
41	40, 8, 37	wrex 2545	. . . . . 6 wff E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. e e. ( EE ` n ) E. f e. ( EE ` n ) ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ( <. a , b >.Cgr <. d , e >. /\ <. a , c >.Cgr <. d , f >. /\ <. b , c >.Cgr <. e , f >. ) )
42	41, 6, 37	wrex 2545	. . . . 5 wff E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. e e. ( EE ` n ) E. f e. ( EE ` n ) ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ( <. a , b >.Cgr <. d , e >. /\ <. a , c >.Cgr <. d , f >. /\ <. b , c >.Cgr <. e , f >. ) )
43	42, 4, 37	wrex 2545	. . . 4 wff E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. e e. ( EE ` n ) E. f e. ( EE ` n ) ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ( <. a , b >.Cgr <. d , e >. /\ <. a , c >.Cgr <. d , f >. /\ <. b , c >.Cgr <. e , f >. ) )
44		cn 9742	. . . 4 class NN
45	43, 34, 44	wrex 2545	. . 3 wff E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. e e. ( EE ` n ) E. f e. ( EE ` n ) ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ( <. a , b >.Cgr <. d , e >. /\ <. a , c >.Cgr <. d , f >. /\ <. b , c >.Cgr <. e , f >. ) )
46	45, 2, 13	copab 4077	. 2 class { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. e e. ( EE ` n ) E. f e. ( EE ` n ) ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ( <. a , b >.Cgr <. d , e >. /\ <. a , c >.Cgr <. d , f >. /\ <. b , c >.Cgr <. e , f >. ) ) }
47	1, 46	wceq 1623	1 wff Cgr3 = { <. p , q >. | E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) E. c e. ( EE ` n ) E. d e. ( EE ` n ) E. e e. ( EE ` n ) E. f e. ( EE ` n ) ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ( <. a , b >.Cgr <. d , e >. /\ <. a , c >.Cgr <. d , f >. /\ <. b , c >.Cgr <. e , f >. ) ) }

This definition is referenced by:  brcgr3  24079