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 ⟨ 𝐸 , 𝐹 ⟩ ) ) )