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 >. ) ) )