# Metamath Proof Explorer

## Theorem brcgr3

Description: Binary relation form of the three-place congruence predicate. (Contributed by Scott Fenton, 4-Oct-2013)

Ref Expression
Assertion 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

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