Theorem brcgr3 32153

Description: Binary relation 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.

Step	Hyp	Ref	Expression
1		opeq1 4402	. . . 4 |- ( a = A -> <. a , b >. = <. A , b >. )
2	1	breq1d 4663	. . 3 |- ( a = A -> ( <. a , b >.Cgr <. d , e >. <-> <. A , b >.Cgr <. d , e >. ) )
3		opeq1 4402	. . . 4 |- ( a = A -> <. a , c >. = <. A , c >. )
4	3	breq1d 4663	. . 3 |- ( a = A -> ( <. a , c >.Cgr <. d , f >. <-> <. A , c >.Cgr <. d , f >. ) )
5	2, 4	3anbi12d 1400	. 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 4403	. . . 4 |- ( b = B -> <. A , b >. = <. A , B >. )
7	6	breq1d 4663	. . 3 |- ( b = B -> ( <. A , b >.Cgr <. d , e >. <-> <. A , B >.Cgr <. d , e >. ) )
8		opeq1 4402	. . . 4 |- ( b = B -> <. b , c >. = <. B , c >. )
9	8	breq1d 4663	. . 3 |- ( b = B -> ( <. b , c >.Cgr <. e , f >. <-> <. B , c >.Cgr <. e , f >. ) )
10	7, 9	3anbi13d 1401	. 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 4403	. . . 4 |- ( c = C -> <. A , c >. = <. A , C >. )
12	11	breq1d 4663	. . 3 |- ( c = C -> ( <. A , c >.Cgr <. d , f >. <-> <. A , C >.Cgr <. d , f >. ) )
13		opeq2 4403	. . . 4 |- ( c = C -> <. B , c >. = <. B , C >. )
14	13	breq1d 4663	. . 3 |- ( c = C -> ( <. B , c >.Cgr <. e , f >. <-> <. B , C >.Cgr <. e , f >. ) )
15	12, 14	3anbi23d 1402	. 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 4402	. . . 4 |- ( d = D -> <. d , e >. = <. D , e >. )
17	16	breq2d 4665	. . 3 |- ( d = D -> ( <. A , B >.Cgr <. d , e >. <-> <. A , B >.Cgr <. D , e >. ) )
18		opeq1 4402	. . . 4 |- ( d = D -> <. d , f >. = <. D , f >. )
19	18	breq2d 4665	. . 3 |- ( d = D -> ( <. A , C >.Cgr <. d , f >. <-> <. A , C >.Cgr <. D , f >. ) )
20	17, 19	3anbi12d 1400	. 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 4403	. . . 4 |- ( e = E -> <. D , e >. = <. D , E >. )
22	21	breq2d 4665	. . 3 |- ( e = E -> ( <. A , B >.Cgr <. D , e >. <-> <. A , B >.Cgr <. D , E >. ) )
23		opeq1 4402	. . . 4 |- ( e = E -> <. e , f >. = <. E , f >. )
24	23	breq2d 4665	. . 3 |- ( e = E -> ( <. B , C >.Cgr <. e , f >. <-> <. B , C >.Cgr <. E , f >. ) )
25	22, 24	3anbi13d 1401	. 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 4403	. . . 4 |- ( f = F -> <. D , f >. = <. D , F >. )
27	26	breq2d 4665	. . 3 |- ( f = F -> ( <. A , C >.Cgr <. D , f >. <-> <. A , C >.Cgr <. D , F >. ) )
28		opeq2 4403	. . . 4 |- ( f = F -> <. E , f >. = <. E , F >. )
29	28	breq2d 4665	. . 3 |- ( f = F -> ( <. B , C >.Cgr <. E , f >. <-> <. B , C >.Cgr <. E , F >. ) )
30	27, 29	3anbi23d 1402	. 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 6191	. 2 |- ( n = N -> ( EE ` n ) = ( EE ` N ) )
32		df-cgr3 32148	. 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 >. ) ) }
33	5, 10, 15, 20, 25, 30, 31, 32	br6 31647	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 >. ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ w3a 1037   = wceq 1483   e. wcel 1990   <.cop 4183   class class class wbr 4653   ` cfv 5888   NNcn 11020   EEcee 25768  Cgrccgr 25770  Cgr3ccgr3 32143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-iota 5851  df-fv 5896  df-cgr3 32148

This theorem is referenced by:  cgr3permute3  32154  cgr3permute1  32155  cgr3tr4  32159  cgr3com  32160  cgr3rflx  32161  cgrxfr  32162  btwnxfr  32163  lineext  32183  brofs2  32184  brifs2  32185  endofsegid  32192  btwnconn1lem4  32197  btwnconn1lem8  32201  btwnconn1lem11  32204  brsegle2  32216  seglecgr12im  32217  segletr  32221