Metamath Proof Explorer

Definition df-cgr3

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)

Ref Expression
Assertion 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 >. ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccgr3 
 |-  Cgr3
1 vp 
 |-  p
2 vq 
 |-  q
3 vn 
 |-  n
4 cn 
 |-  NN
5 va 
 |-  a
6 cee 
 |-  EE
7 3 cv 
 |-  n
8 7 6 cfv 
 |-  ( EE ` n )
9 vb 
 |-  b
10 vc 
 |-  c
11 vd 
 |-  d
12 ve 
 |-  e
13 vf 
 |-  f
14 1 cv 
 |-  p
15 5 cv 
 |-  a
16 9 cv 
 |-  b
17 10 cv 
 |-  c
18 16 17 cop 
 |-  <. b , c >.
19 15 18 cop 
 |-  <. a , <. b , c >. >.
20 14 19 wceq 
 |-  p = <. a , <. b , c >. >.
21 2 cv 
 |-  q
22 11 cv 
 |-  d
23 12 cv 
 |-  e
24 13 cv 
 |-  f
25 23 24 cop 
 |-  <. e , f >.
26 22 25 cop 
 |-  <. d , <. e , f >. >.
27 21 26 wceq 
 |-  q = <. d , <. e , f >. >.
28 15 16 cop 
 |-  <. a , b >.
29 ccgr 
 |-  Cgr
30 22 23 cop 
 |-  <. d , e >.
31 28 30 29 wbr 
 |-  <. a , b >. Cgr <. d , e >.
32 15 17 cop 
 |-  <. a , c >.
33 22 24 cop 
 |-  <. d , f >.
34 32 33 29 wbr 
 |-  <. a , c >. Cgr <. d , f >.
35 18 25 29 wbr 
 |-  <. b , c >. Cgr <. e , f >.
36 31 34 35 w3a 
 |-  ( <. a , b >. Cgr <. d , e >. /\ <. a , c >. Cgr <. d , f >. /\ <. b , c >. Cgr <. e , f >. )
37 20 27 36 w3a 
 |-  ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ( <. a , b >. Cgr <. d , e >. /\ <. a , c >. Cgr <. d , f >. /\ <. b , c >. Cgr <. e , f >. ) )
38 37 13 8 wrex 
 |-  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 12 8 wrex 
 |-  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 11 8 wrex 
 |-  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 10 8 wrex 
 |-  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 9 8 wrex 
 |-  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 5 8 wrex 
 |-  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 43 3 4 wrex 
 |-  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 >. ) )
45 44 1 2 copab 
 |-  { <. 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 >. ) ) }
46 0 45 wceq 
 |-  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 >. ) ) }