# 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 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},⟨{B},{C}⟩⟩\mathrm{Cgr3}⟨{D},⟨{E},{F}⟩⟩↔\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)$

### Proof

Step Hyp Ref Expression
1 opeq1 ${⊢}{a}={A}\to ⟨{a},{b}⟩=⟨{A},{b}⟩$
2 1 breq1d ${⊢}{a}={A}\to \left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩↔⟨{A},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\right)$
3 opeq1 ${⊢}{a}={A}\to ⟨{a},{c}⟩=⟨{A},{c}⟩$
4 3 breq1d ${⊢}{a}={A}\to \left(⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩↔⟨{A},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\right)$
5 2 4 3anbi12d ${⊢}{a}={A}\to \left(\left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)↔\left(⟨{A},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{A},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)$
6 opeq2 ${⊢}{b}={B}\to ⟨{A},{b}⟩=⟨{A},{B}⟩$
7 6 breq1d ${⊢}{b}={B}\to \left(⟨{A},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩↔⟨{A},{B}⟩\mathrm{Cgr}⟨{d},{e}⟩\right)$
8 opeq1 ${⊢}{b}={B}\to ⟨{b},{c}⟩=⟨{B},{c}⟩$
9 8 breq1d ${⊢}{b}={B}\to \left(⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩↔⟨{B},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)$
10 7 9 3anbi13d ${⊢}{b}={B}\to \left(\left(⟨{A},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{A},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)↔\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{A},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{B},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)$
11 opeq2 ${⊢}{c}={C}\to ⟨{A},{c}⟩=⟨{A},{C}⟩$
12 11 breq1d ${⊢}{c}={C}\to \left(⟨{A},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩↔⟨{A},{C}⟩\mathrm{Cgr}⟨{d},{f}⟩\right)$
13 opeq2 ${⊢}{c}={C}\to ⟨{B},{c}⟩=⟨{B},{C}⟩$
14 13 breq1d ${⊢}{c}={C}\to \left(⟨{B},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩↔⟨{B},{C}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)$
15 12 14 3anbi23d ${⊢}{c}={C}\to \left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{A},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{B},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)↔\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)$
16 opeq1 ${⊢}{d}={D}\to ⟨{d},{e}⟩=⟨{D},{e}⟩$
17 16 breq2d ${⊢}{d}={D}\to \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{d},{e}⟩↔⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{e}⟩\right)$
18 opeq1 ${⊢}{d}={D}\to ⟨{d},{f}⟩=⟨{D},{f}⟩$
19 18 breq2d ${⊢}{d}={D}\to \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{d},{f}⟩↔⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{f}⟩\right)$
20 17 19 3anbi12d ${⊢}{d}={D}\to \left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)↔\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{e}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{f}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)$
21 opeq2 ${⊢}{e}={E}\to ⟨{D},{e}⟩=⟨{D},{E}⟩$
22 21 breq2d ${⊢}{e}={E}\to \left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{e}⟩↔⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\right)$
23 opeq1 ${⊢}{e}={E}\to ⟨{e},{f}⟩=⟨{E},{f}⟩$
24 23 breq2d ${⊢}{e}={E}\to \left(⟨{B},{C}⟩\mathrm{Cgr}⟨{e},{f}⟩↔⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{f}⟩\right)$
25 22 24 3anbi13d ${⊢}{e}={E}\to \left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{e}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{f}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)↔\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{f}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{f}⟩\right)\right)$
26 opeq2 ${⊢}{f}={F}\to ⟨{D},{f}⟩=⟨{D},{F}⟩$
27 26 breq2d ${⊢}{f}={F}\to \left(⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{f}⟩↔⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\right)$
28 opeq2 ${⊢}{f}={F}\to ⟨{E},{f}⟩=⟨{E},{F}⟩$
29 28 breq2d ${⊢}{f}={F}\to \left(⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{f}⟩↔⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)$
30 27 29 3anbi23d ${⊢}{f}={F}\to \left(\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{f}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{f}⟩\right)↔\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)$
31 fveq2 ${⊢}{n}={N}\to 𝔼\left({n}\right)=𝔼\left({N}\right)$
32 df-cgr3 ${⊢}\mathrm{Cgr3}=\left\{⟨{p},{q}⟩|\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {a}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {b}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {c}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {d}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {e}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\exists {f}\in 𝔼\left({n}\right)\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge \left(⟨{a},{b}⟩\mathrm{Cgr}⟨{d},{e}⟩\wedge ⟨{a},{c}⟩\mathrm{Cgr}⟨{d},{f}⟩\wedge ⟨{b},{c}⟩\mathrm{Cgr}⟨{e},{f}⟩\right)\right)\right\}$
33 5 10 15 20 25 30 31 32 br6 ${⊢}\left({N}\in ℕ\wedge \left({A}\in 𝔼\left({N}\right)\wedge {B}\in 𝔼\left({N}\right)\wedge {C}\in 𝔼\left({N}\right)\right)\wedge \left({D}\in 𝔼\left({N}\right)\wedge {E}\in 𝔼\left({N}\right)\wedge {F}\in 𝔼\left({N}\right)\right)\right)\to \left(⟨{A},⟨{B},{C}⟩⟩\mathrm{Cgr3}⟨{D},⟨{E},{F}⟩⟩↔\left(⟨{A},{B}⟩\mathrm{Cgr}⟨{D},{E}⟩\wedge ⟨{A},{C}⟩\mathrm{Cgr}⟨{D},{F}⟩\wedge ⟨{B},{C}⟩\mathrm{Cgr}⟨{E},{F}⟩\right)\right)$