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

Theorem brcgr3 28214
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 4160 . . . 4  |-  ( a  =  A  ->  <. a ,  b >.  =  <. A ,  b >. )
21breq1d 4403 . . 3  |-  ( a  =  A  ->  ( <. a ,  b >.Cgr <. d ,  e >.  <->  <. A ,  b >.Cgr <.
d ,  e >.
) )
3 opeq1 4160 . . . 4  |-  ( a  =  A  ->  <. a ,  c >.  =  <. A ,  c >. )
43breq1d 4403 . . 3  |-  ( a  =  A  ->  ( <. a ,  c >.Cgr <. d ,  f >.  <->  <. A ,  c >.Cgr <.
d ,  f >.
) )
52, 43anbi12d 1291 . 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 4161 . . . 4  |-  ( b  =  B  ->  <. A , 
b >.  =  <. A ,  B >. )
76breq1d 4403 . . 3  |-  ( b  =  B  ->  ( <. A ,  b >.Cgr <. d ,  e >.  <->  <. A ,  B >.Cgr <.
d ,  e >.
) )
8 opeq1 4160 . . . 4  |-  ( b  =  B  ->  <. b ,  c >.  =  <. B ,  c >. )
98breq1d 4403 . . 3  |-  ( b  =  B  ->  ( <. b ,  c >.Cgr <. e ,  f >.  <->  <. B ,  c >.Cgr <.
e ,  f >.
) )
107, 93anbi13d 1292 . 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 4161 . . . 4  |-  ( c  =  C  ->  <. A , 
c >.  =  <. A ,  C >. )
1211breq1d 4403 . . 3  |-  ( c  =  C  ->  ( <. A ,  c >.Cgr <. d ,  f >.  <->  <. A ,  C >.Cgr <.
d ,  f >.
) )
13 opeq2 4161 . . . 4  |-  ( c  =  C  ->  <. B , 
c >.  =  <. B ,  C >. )
1413breq1d 4403 . . 3  |-  ( c  =  C  ->  ( <. B ,  c >.Cgr <. e ,  f >.  <->  <. B ,  C >.Cgr <.
e ,  f >.
) )
1512, 143anbi23d 1293 . 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 4160 . . . 4  |-  ( d  =  D  ->  <. d ,  e >.  =  <. D ,  e >. )
1716breq2d 4405 . . 3  |-  ( d  =  D  ->  ( <. A ,  B >.Cgr <.
d ,  e >.  <->  <. A ,  B >.Cgr <. D ,  e >. ) )
18 opeq1 4160 . . . 4  |-  ( d  =  D  ->  <. d ,  f >.  =  <. D ,  f >. )
1918breq2d 4405 . . 3  |-  ( d  =  D  ->  ( <. A ,  C >.Cgr <.
d ,  f >.  <->  <. A ,  C >.Cgr <. D ,  f >. ) )
2017, 193anbi12d 1291 . 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 4161 . . . 4  |-  ( e  =  E  ->  <. D , 
e >.  =  <. D ,  E >. )
2221breq2d 4405 . . 3  |-  ( e  =  E  ->  ( <. A ,  B >.Cgr <. D ,  e >.  <->  <. A ,  B >.Cgr <. D ,  E >. ) )
23 opeq1 4160 . . . 4  |-  ( e  =  E  ->  <. e ,  f >.  =  <. E ,  f >. )
2423breq2d 4405 . . 3  |-  ( e  =  E  ->  ( <. B ,  C >.Cgr <.
e ,  f >.  <->  <. B ,  C >.Cgr <. E ,  f >. ) )
2522, 243anbi13d 1292 . 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 4161 . . . 4  |-  ( f  =  F  ->  <. D , 
f >.  =  <. D ,  F >. )
2726breq2d 4405 . . 3  |-  ( f  =  F  ->  ( <. A ,  C >.Cgr <. D ,  f >.  <->  <. A ,  C >.Cgr <. D ,  F >. ) )
28 opeq2 4161 . . . 4  |-  ( f  =  F  ->  <. E , 
f >.  =  <. E ,  F >. )
2928breq2d 4405 . . 3  |-  ( f  =  F  ->  ( <. B ,  C >.Cgr <. E ,  f >.  <->  <. B ,  C >.Cgr <. E ,  F >. ) )
3027, 293anbi23d 1293 . 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 5792 . 2  |-  ( n  =  N  ->  ( EE `  n )  =  ( EE `  N
) )
32 df-cgr3 28209 . 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 27704 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 setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 965    = wceq 1370    e. wcel 1758   <.cop 3984   class class class wbr 4393   ` cfv 5519   NNcn 10426   EEcee 23279  Cgrccgr 23281  Cgr3ccgr3 28204
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pr 4632
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-opab 4452  df-iota 5482  df-fv 5527  df-cgr3 28209
This theorem is referenced by:  cgr3permute3  28215  cgr3permute1  28216  cgr3tr4  28220  cgr3com  28221  cgr3rflx  28222  cgrxfr  28223  btwnxfr  28224  lineext  28244  brofs2  28245  brifs2  28246  endofsegid  28253  btwnconn1lem4  28258  btwnconn1lem8  28262  btwnconn1lem11  28265  brsegle2  28277  seglecgr12im  28278  segletr  28282
  Copyright terms: Public domain W3C validator