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

Theorem brcgr3 25888
Description: Binary relationship form of the three-place congruence predicate. (Contributed by Scott Fenton, 4-Oct-2013.)
Assertion
Ref Expression
brcgr3  |-  ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  ->  ( <. A ,  <. B ,  C >. >.Cgr3 <. D ,  <. E ,  F >. >.  <->  ( <. A ,  B >.Cgr <. D ,  E >.  /\  <. A ,  C >.Cgr <. D ,  F >.  /\  <. B ,  C >.Cgr
<. E ,  F >. ) ) )

Proof of Theorem brcgr3
Dummy variables  a 
b  c  d  e  f  n  p  q are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq1 3948 . . . 4  |-  ( a  =  A  ->  <. a ,  b >.  =  <. A ,  b >. )
21breq1d 4186 . . 3  |-  ( a  =  A  ->  ( <. a ,  b >.Cgr <. d ,  e >.  <->  <. A ,  b >.Cgr <.
d ,  e >.
) )
3 opeq1 3948 . . . 4  |-  ( a  =  A  ->  <. a ,  c >.  =  <. A ,  c >. )
43breq1d 4186 . . 3  |-  ( a  =  A  ->  ( <. a ,  c >.Cgr <. d ,  f >.  <->  <. A ,  c >.Cgr <.
d ,  f >.
) )
52, 43anbi12d 1255 . 2  |-  ( a  =  A  ->  (
( <. a ,  b
>.Cgr <. d ,  e
>.  /\  <. a ,  c
>.Cgr <. d ,  f
>.  /\  <. b ,  c
>.Cgr <. e ,  f
>. )  <->  ( <. A , 
b >.Cgr <. d ,  e
>.  /\  <. A ,  c
>.Cgr <. d ,  f
>.  /\  <. b ,  c
>.Cgr <. e ,  f
>. ) ) )
6 opeq2 3949 . . . 4  |-  ( b  =  B  ->  <. A , 
b >.  =  <. A ,  B >. )
76breq1d 4186 . . 3  |-  ( b  =  B  ->  ( <. A ,  b >.Cgr <. d ,  e >.  <->  <. A ,  B >.Cgr <.
d ,  e >.
) )
8 opeq1 3948 . . . 4  |-  ( b  =  B  ->  <. b ,  c >.  =  <. B ,  c >. )
98breq1d 4186 . . 3  |-  ( b  =  B  ->  ( <. b ,  c >.Cgr <. e ,  f >.  <->  <. B ,  c >.Cgr <.
e ,  f >.
) )
107, 93anbi13d 1256 . 2  |-  ( b  =  B  ->  (
( <. A ,  b
>.Cgr <. d ,  e
>.  /\  <. A ,  c
>.Cgr <. d ,  f
>.  /\  <. b ,  c
>.Cgr <. e ,  f
>. )  <->  ( <. A ,  B >.Cgr <. d ,  e
>.  /\  <. A ,  c
>.Cgr <. d ,  f
>.  /\  <. B ,  c
>.Cgr <. e ,  f
>. ) ) )
11 opeq2 3949 . . . 4  |-  ( c  =  C  ->  <. A , 
c >.  =  <. A ,  C >. )
1211breq1d 4186 . . 3  |-  ( c  =  C  ->  ( <. A ,  c >.Cgr <. d ,  f >.  <->  <. A ,  C >.Cgr <.
d ,  f >.
) )
13 opeq2 3949 . . . 4  |-  ( c  =  C  ->  <. B , 
c >.  =  <. B ,  C >. )
1413breq1d 4186 . . 3  |-  ( c  =  C  ->  ( <. B ,  c >.Cgr <. e ,  f >.  <->  <. B ,  C >.Cgr <.
e ,  f >.
) )
1512, 143anbi23d 1257 . 2  |-  ( c  =  C  ->  (
( <. A ,  B >.Cgr
<. d ,  e >.  /\  <. A ,  c
>.Cgr <. d ,  f
>.  /\  <. B ,  c
>.Cgr <. e ,  f
>. )  <->  ( <. A ,  B >.Cgr <. d ,  e
>.  /\  <. A ,  C >.Cgr
<. d ,  f >.  /\  <. B ,  C >.Cgr
<. e ,  f >.
) ) )
16 opeq1 3948 . . . 4  |-  ( d  =  D  ->  <. d ,  e >.  =  <. D ,  e >. )
1716breq2d 4188 . . 3  |-  ( d  =  D  ->  ( <. A ,  B >.Cgr <.
d ,  e >.  <->  <. A ,  B >.Cgr <. D ,  e >. ) )
18 opeq1 3948 . . . 4  |-  ( d  =  D  ->  <. d ,  f >.  =  <. D ,  f >. )
1918breq2d 4188 . . 3  |-  ( d  =  D  ->  ( <. A ,  C >.Cgr <.
d ,  f >.  <->  <. A ,  C >.Cgr <. D ,  f >. ) )
2017, 193anbi12d 1255 . 2  |-  ( d  =  D  ->  (
( <. A ,  B >.Cgr
<. d ,  e >.  /\  <. A ,  C >.Cgr
<. d ,  f >.  /\  <. B ,  C >.Cgr
<. e ,  f >.
)  <->  ( <. A ,  B >.Cgr <. D ,  e
>.  /\  <. A ,  C >.Cgr
<. D ,  f >.  /\  <. B ,  C >.Cgr
<. e ,  f >.
) ) )
21 opeq2 3949 . . . 4  |-  ( e  =  E  ->  <. D , 
e >.  =  <. D ,  E >. )
2221breq2d 4188 . . 3  |-  ( e  =  E  ->  ( <. A ,  B >.Cgr <. D ,  e >.  <->  <. A ,  B >.Cgr <. D ,  E >. ) )
23 opeq1 3948 . . . 4  |-  ( e  =  E  ->  <. e ,  f >.  =  <. E ,  f >. )
2423breq2d 4188 . . 3  |-  ( e  =  E  ->  ( <. B ,  C >.Cgr <.
e ,  f >.  <->  <. B ,  C >.Cgr <. E ,  f >. ) )
2522, 243anbi13d 1256 . 2  |-  ( e  =  E  ->  (
( <. A ,  B >.Cgr
<. D ,  e >.  /\  <. A ,  C >.Cgr
<. D ,  f >.  /\  <. B ,  C >.Cgr
<. e ,  f >.
)  <->  ( <. A ,  B >.Cgr <. D ,  E >.  /\  <. A ,  C >.Cgr
<. D ,  f >.  /\  <. B ,  C >.Cgr
<. E ,  f >.
) ) )
26 opeq2 3949 . . . 4  |-  ( f  =  F  ->  <. D , 
f >.  =  <. D ,  F >. )
2726breq2d 4188 . . 3  |-  ( f  =  F  ->  ( <. A ,  C >.Cgr <. D ,  f >.  <->  <. A ,  C >.Cgr <. D ,  F >. ) )
28 opeq2 3949 . . . 4  |-  ( f  =  F  ->  <. E , 
f >.  =  <. E ,  F >. )
2928breq2d 4188 . . 3  |-  ( f  =  F  ->  ( <. B ,  C >.Cgr <. E ,  f >.  <->  <. B ,  C >.Cgr <. E ,  F >. ) )
3027, 293anbi23d 1257 . 2  |-  ( f  =  F  ->  (
( <. A ,  B >.Cgr
<. D ,  E >.  /\ 
<. A ,  C >.Cgr <. D ,  f >.  /\ 
<. B ,  C >.Cgr <. E ,  f >. )  <-> 
( <. A ,  B >.Cgr
<. D ,  E >.  /\ 
<. A ,  C >.Cgr <. D ,  F >.  /\ 
<. B ,  C >.Cgr <. E ,  F >. ) ) )
31 fveq2 5691 . 2  |-  ( n  =  N  ->  ( EE `  n )  =  ( EE `  N
) )
32 df-cgr3 25882 . 2  |- 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
>. ) ) }
335, 10, 15, 20, 25, 30, 31, 32br6 25332 1  |-  ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  ->  ( <. A ,  <. B ,  C >. >.Cgr3 <. D ,  <. E ,  F >. >.  <->  ( <. A ,  B >.Cgr <. D ,  E >.  /\  <. A ,  C >.Cgr <. D ,  F >.  /\  <. B ,  C >.Cgr
<. E ,  F >. ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936    = wceq 1649    e. wcel 1721   <.cop 3781   class class class wbr 4176   ` cfv 5417   NNcn 9960   EEcee 25735  Cgrccgr 25737  Cgr3ccgr3 25878
This theorem is referenced by:  cgr3permute3  25889  cgr3permute1  25890  cgr3tr4  25894  cgr3com  25895  cgr3rflx  25896  cgrxfr  25897  btwnxfr  25898  lineext  25918  brofs2  25919  brifs2  25920  endofsegid  25927  btwnconn1lem4  25932  btwnconn1lem8  25936  btwnconn1lem11  25939  brsegle2  25951  seglecgr12im  25952  segletr  25956
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-iota 5381  df-fv 5425  df-cgr3 25882
  Copyright terms: Public domain W3C validator