Theorem brcgr3 33897

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ⟨cop 4528   class class class wbr 5032  ‘cfv 6335  ℕcn 11674  𝔼cee 26781  Cgrccgr 26783  Cgr3ccgr3 33887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rex 3076  df-v 3411  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-iota 6294  df-fv 6343  df-cgr3 33892

This theorem is referenced by:  cgr3permute3  33898  cgr3permute1  33899  cgr3tr4  33903  cgr3com  33904  cgr3rflx  33905  cgrxfr  33906  btwnxfr  33907  lineext  33927  brofs2  33928  brifs2  33929  endofsegid  33936  btwnconn1lem4  33941  btwnconn1lem8  33945  btwnconn1lem11  33948  brsegle2  33960  seglecgr12im  33961  segletr  33965