Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cgr3 Unicode version

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
StepHypRef Expression
1 ccgr3 24069 . 2  class Cgr3
2 vp . . . . . . . . . . . . 13  set  p
32cv 1622 . . . . . . . . . . . 12  class  p
4 va . . . . . . . . . . . . . 14  set  a
54cv 1622 . . . . . . . . . . . . 13  class  a
6 vb . . . . . . . . . . . . . . 15  set  b
76cv 1622 . . . . . . . . . . . . . 14  class  b
8 vc . . . . . . . . . . . . . . 15  set  c
98cv 1622 . . . . . . . . . . . . . 14  class  c
107, 9cop 3644 . . . . . . . . . . . . 13  class  <. b ,  c >.
115, 10cop 3644 . . . . . . . . . . . 12  class  <. a ,  <. b ,  c
>. >.
123, 11wceq 1623 . . . . . . . . . . 11  wff  p  = 
<. a ,  <. b ,  c >. >.
13 vq . . . . . . . . . . . . 13  set  q
1413cv 1622 . . . . . . . . . . . 12  class  q
15 vd . . . . . . . . . . . . . 14  set  d
1615cv 1622 . . . . . . . . . . . . 13  class  d
17 ve . . . . . . . . . . . . . . 15  set  e
1817cv 1622 . . . . . . . . . . . . . 14  class  e
19 vf . . . . . . . . . . . . . . 15  set  f
2019cv 1622 . . . . . . . . . . . . . 14  class  f
2118, 20cop 3644 . . . . . . . . . . . . 13  class  <. e ,  f >.
2216, 21cop 3644 . . . . . . . . . . . 12  class  <. d ,  <. e ,  f
>. >.
2314, 22wceq 1623 . . . . . . . . . . 11  wff  q  = 
<. d ,  <. e ,  f >. >.
245, 7cop 3644 . . . . . . . . . . . . 13  class  <. a ,  b >.
2516, 18cop 3644 . . . . . . . . . . . . 13  class  <. d ,  e >.
26 ccgr 23928 . . . . . . . . . . . . 13  class Cgr
2724, 25, 26wbr 4024 . . . . . . . . . . . 12  wff  <. a ,  b >.Cgr <. d ,  e >.
285, 9cop 3644 . . . . . . . . . . . . 13  class  <. a ,  c >.
2916, 20cop 3644 . . . . . . . . . . . . 13  class  <. d ,  f >.
3028, 29, 26wbr 4024 . . . . . . . . . . . 12  wff  <. a ,  c >.Cgr <. d ,  f >.
3110, 21, 26wbr 4024 . . . . . . . . . . . 12  wff  <. b ,  c >.Cgr <. e ,  f >.
3227, 30, 31w3a 934 . . . . . . . . . . 11  wff  ( <.
a ,  b >.Cgr <. d ,  e >.  /\  <. a ,  c
>.Cgr <. d ,  f
>.  /\  <. b ,  c
>.Cgr <. e ,  f
>. )
3312, 23, 32w3a 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
3534cv 1622 . . . . . . . . . . 11  class  n
36 cee 23926 . . . . . . . . . . 11  class  EE
3735, 36cfv 5221 . . . . . . . . . 10  class  ( EE
`  n )
3833, 19, 37wrex 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
>. ) )
3938, 17, 37wrex 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
>. ) )
4039, 15, 37wrex 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
>. ) )
4140, 8, 37wrex 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
>. ) )
4241, 6, 37wrex 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
>. ) )
4342, 4, 37wrex 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
4543, 34, 44wrex 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
>. ) )
4645, 2, 13copab 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
>. ) ) }
471, 46wceq 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
>. ) ) }
Colors of variables: wff set class
This definition is referenced by:  brcgr3  24079
  Copyright terms: Public domain W3C validator