Theorem brcgr3 36656

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 4833	. . . 4 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
2	1	breq1d 5113	. . 3 ⊢ (𝑎 = 𝐴 → (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ↔ ⟨𝐴, 𝑏⟩Cgr⟨𝑑, 𝑒⟩))
3		opeq1 4833	. . . 4 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑐⟩ = ⟨𝐴, 𝑐⟩)
4	3	breq1d 5113	. . 3 ⊢ (𝑎 = 𝐴 → (⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ↔ ⟨𝐴, 𝑐⟩Cgr⟨𝑑, 𝑓⟩))
5	2, 4	3anbi12d 1465	. 2 ⊢ (𝑎 = 𝐴 → ((⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩) ↔ (⟨𝐴, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝐴, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩)))
6		opeq2 4834	. . . 4 ⊢ (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
7	6	breq1d 5113	. . 3 ⊢ (𝑏 = 𝐵 → (⟨𝐴, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝑑, 𝑒⟩))
8		opeq1 4833	. . . 4 ⊢ (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
9	8	breq1d 5113	. . 3 ⊢ (𝑏 = 𝐵 → (⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩ ↔ ⟨𝐵, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
10	7, 9	3anbi13d 1466	. 2 ⊢ (𝑏 = 𝐵 → ((⟨𝐴, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝐴, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝐴, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑒, 𝑓⟩)))
11		opeq2 4834	. . . 4 ⊢ (𝑐 = 𝐶 → ⟨𝐴, 𝑐⟩ = ⟨𝐴, 𝐶⟩)
12	11	breq1d 5113	. . 3 ⊢ (𝑐 = 𝐶 → (⟨𝐴, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝑑, 𝑓⟩))
13		opeq2 4834	. . . 4 ⊢ (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
14	13	breq1d 5113	. . 3 ⊢ (𝑐 = 𝐶 → (⟨𝐵, 𝑐⟩Cgr⟨𝑒, 𝑓⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝑓⟩))
15	12, 14	3anbi23d 1467	. 2 ⊢ (𝑐 = 𝐶 → ((⟨𝐴, 𝐵⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝐴, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑒, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝑓⟩)))
16		opeq1 4833	. . . 4 ⊢ (𝑑 = 𝐷 → ⟨𝑑, 𝑒⟩ = ⟨𝐷, 𝑒⟩)
17	16	breq2d 5115	. . 3 ⊢ (𝑑 = 𝐷 → (⟨𝐴, 𝐵⟩Cgr⟨𝑑, 𝑒⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝑒⟩))
18		opeq1 4833	. . . 4 ⊢ (𝑑 = 𝐷 → ⟨𝑑, 𝑓⟩ = ⟨𝐷, 𝑓⟩)
19	18	breq2d 5115	. . 3 ⊢ (𝑑 = 𝐷 → (⟨𝐴, 𝐶⟩Cgr⟨𝑑, 𝑓⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝑓⟩))
20	17, 19	3anbi12d 1465	. 2 ⊢ (𝑑 = 𝐷 → ((⟨𝐴, 𝐵⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝑒⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝑓⟩)))
21		opeq2 4834	. . . 4 ⊢ (𝑒 = 𝐸 → ⟨𝐷, 𝑒⟩ = ⟨𝐷, 𝐸⟩)
22	21	breq2d 5115	. . 3 ⊢ (𝑒 = 𝐸 → (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝑒⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩))
23		opeq1 4833	. . . 4 ⊢ (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩)
24	23	breq2d 5115	. . 3 ⊢ (𝑒 = 𝐸 → (⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝑓⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝑓⟩))
25	22, 24	3anbi13d 1466	. 2 ⊢ (𝑒 = 𝐸 → ((⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝑒⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝑓⟩)))
26		opeq2 4834	. . . 4 ⊢ (𝑓 = 𝐹 → ⟨𝐷, 𝑓⟩ = ⟨𝐷, 𝐹⟩)
27	26	breq2d 5115	. . 3 ⊢ (𝑓 = 𝐹 → (⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝑓⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩))
28		opeq2 4834	. . . 4 ⊢ (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩)
29	28	breq2d 5115	. . 3 ⊢ (𝑓 = 𝐹 → (⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝑓⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝐹⟩))
30	27, 29	3anbi23d 1467	. 2 ⊢ (𝑓 = 𝐹 → ((⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝐹⟩)))
31		fveq2 6880	. 2 ⊢ (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁))
32		df-cgr3 36651	. 2 ⊢ Cgr3 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))}
33	5, 10, 15, 20, 25, 30, 31, 32	br6 36366	1 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝐹⟩)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ⟨cop 4590   class class class wbr 5103  ‘cfv 6534  ℕcn 12279  𝔼cee 29373  Cgrccgr 29375  Cgr3ccgr3 36646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-iota 6490  df-fv 6542  df-cgr3 36651

This theorem is used by:  cgr3permute3  36657  cgr3permute1  36658  cgr3tr4  36662  cgr3com  36663  cgr3rflx  36664  cgrxfr  36665  btwnxfr  36666  lineext  36686  brofs2  36687  brifs2  36688  endofsegid  36695  btwnconn1lem4  36700  btwnconn1lem8  36704  btwnconn1lem11  36707  brsegle2  36719  seglecgr12im  36720  segletr  36724