Theorem brcgr3 35487

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

Assertion

Ref	Expression
brcgr3	⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝐹⟩)))

Proof of Theorem brcgr3

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑛 𝑝 𝑞 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  ⟨cop 4634   class class class wbr 5148  ‘cfv 6543  ℕcn 12219  𝔼cee 28578  Cgrccgr 28580  Cgr3ccgr3 35477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-iota 6495  df-fv 6551  df-cgr3 35482

This theorem is referenced by:  cgr3permute3  35488  cgr3permute1  35489  cgr3tr4  35493  cgr3com  35494  cgr3rflx  35495  cgrxfr  35496  btwnxfr  35497  lineext  35517  brofs2  35518  brifs2  35519  endofsegid  35526  btwnconn1lem4  35531  btwnconn1lem8  35535  btwnconn1lem11  35538  brsegle2  35550  seglecgr12im  35551  segletr  35555