# 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 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) )

### Proof

Step Hyp Ref Expression
1 opeq1 ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ )
2 1 breq1d ( 𝑎 = 𝐴 → ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ↔ ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ) )
3 opeq1 ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑐 ⟩ = ⟨ 𝐴 , 𝑐 ⟩ )
4 3 breq1d ( 𝑎 = 𝐴 → ( ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ↔ ⟨ 𝐴 , 𝑐 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ) )
5 2 4 3anbi12d ( 𝑎 = 𝐴 → ( ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ∧ ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) ↔ ( ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ∧ ⟨ 𝐴 , 𝑐 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) ) )
6 opeq2 ( 𝑏 = 𝐵 → ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
7 6 breq1d ( 𝑏 = 𝐵 → ( ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ) )
8 opeq1 ( 𝑏 = 𝐵 → ⟨ 𝑏 , 𝑐 ⟩ = ⟨ 𝐵 , 𝑐 ⟩ )
9 8 breq1d ( 𝑏 = 𝐵 → ( ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ↔ ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) )
10 7 9 3anbi13d ( 𝑏 = 𝐵 → ( ( ⟨ 𝐴 , 𝑏 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ∧ ⟨ 𝐴 , 𝑐 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ∧ ⟨ 𝐴 , 𝑐 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) ) )
11 opeq2 ( 𝑐 = 𝐶 → ⟨ 𝐴 , 𝑐 ⟩ = ⟨ 𝐴 , 𝐶 ⟩ )
12 11 breq1d ( 𝑐 = 𝐶 → ( ⟨ 𝐴 , 𝑐 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ↔ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ) )
13 opeq2 ( 𝑐 = 𝐶 → ⟨ 𝐵 , 𝑐 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ )
14 13 breq1d ( 𝑐 = 𝐶 → ( ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) )
15 12 14 3anbi23d ( 𝑐 = 𝐶 → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ∧ ⟨ 𝐴 , 𝑐 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝑐 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) ) )
16 opeq1 ( 𝑑 = 𝐷 → ⟨ 𝑑 , 𝑒 ⟩ = ⟨ 𝐷 , 𝑒 ⟩ )
17 16 breq2d ( 𝑑 = 𝐷 → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑒 ⟩ ) )
18 opeq1 ( 𝑑 = 𝐷 → ⟨ 𝑑 , 𝑓 ⟩ = ⟨ 𝐷 , 𝑓 ⟩ )
19 18 breq2d ( 𝑑 = 𝐷 → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ↔ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝑓 ⟩ ) )
20 17 19 3anbi12d ( 𝑑 = 𝐷 → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑒 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) ) )
21 opeq2 ( 𝑒 = 𝐸 → ⟨ 𝐷 , 𝑒 ⟩ = ⟨ 𝐷 , 𝐸 ⟩ )
22 21 breq2d ( 𝑒 = 𝐸 → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑒 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ) )
23 opeq1 ( 𝑒 = 𝐸 → ⟨ 𝑒 , 𝑓 ⟩ = ⟨ 𝐸 , 𝑓 ⟩ )
24 23 breq2d ( 𝑒 = 𝐸 → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝑓 ⟩ ) )
25 22 24 3anbi13d ( 𝑒 = 𝐸 → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝑒 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝑓 ⟩ ) ) )
26 opeq2 ( 𝑓 = 𝐹 → ⟨ 𝐷 , 𝑓 ⟩ = ⟨ 𝐷 , 𝐹 ⟩ )
27 26 breq2d ( 𝑓 = 𝐹 → ( ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝑓 ⟩ ↔ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ) )
28 opeq2 ( 𝑓 = 𝐹 → ⟨ 𝐸 , 𝑓 ⟩ = ⟨ 𝐸 , 𝐹 ⟩ )
29 28 breq2d ( 𝑓 = 𝐹 → ( ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝑓 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) )
30 27 29 3anbi23d ( 𝑓 = 𝐹 → ( ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝑓 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝑓 ⟩ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) )
31 fveq2 ( 𝑛 = 𝑁 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑁 ) )
32 df-cgr3 Cgr3 = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ ∧ 𝑞 = ⟨ 𝑑 , ⟨ 𝑒 , 𝑓 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ∧ ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) ) }
33 5 10 15 20 25 30 31 32 br6 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , ⟨ 𝐵 , 𝐶 ⟩ ⟩ Cgr3 ⟨ 𝐷 , ⟨ 𝐸 , 𝐹 ⟩ ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐴 , 𝐶 ⟩ Cgr ⟨ 𝐷 , 𝐹 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) )