Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brcgr3 Structured version   Visualization version   GIF version

Theorem brcgr3 32128
Description: Binary relationship 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.
StepHypRef Expression
1 opeq1 4393 . . . 4 (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
21breq1d 4654 . . 3 (𝑎 = 𝐴 → (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ↔ ⟨𝐴, 𝑏⟩Cgr⟨𝑑, 𝑒⟩))
3 opeq1 4393 . . . 4 (𝑎 = 𝐴 → ⟨𝑎, 𝑐⟩ = ⟨𝐴, 𝑐⟩)
43breq1d 4654 . . 3 (𝑎 = 𝐴 → (⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ↔ ⟨𝐴, 𝑐⟩Cgr⟨𝑑, 𝑓⟩))
52, 43anbi12d 1398 . 2 (𝑎 = 𝐴 → ((⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩) ↔ (⟨𝐴, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝐴, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩)))
6 opeq2 4394 . . . 4 (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
76breq1d 4654 . . 3 (𝑏 = 𝐵 → (⟨𝐴, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝑑, 𝑒⟩))
8 opeq1 4393 . . . 4 (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
98breq1d 4654 . . 3 (𝑏 = 𝐵 → (⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩ ↔ ⟨𝐵, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
107, 93anbi13d 1399 . 2 (𝑏 = 𝐵 → ((⟨𝐴, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝐴, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝐴, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑒, 𝑓⟩)))
11 opeq2 4394 . . . 4 (𝑐 = 𝐶 → ⟨𝐴, 𝑐⟩ = ⟨𝐴, 𝐶⟩)
1211breq1d 4654 . . 3 (𝑐 = 𝐶 → (⟨𝐴, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝑑, 𝑓⟩))
13 opeq2 4394 . . . 4 (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
1413breq1d 4654 . . 3 (𝑐 = 𝐶 → (⟨𝐵, 𝑐⟩Cgr⟨𝑒, 𝑓⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝑓⟩))
1512, 143anbi23d 1400 . 2 (𝑐 = 𝐶 → ((⟨𝐴, 𝐵⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝐴, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑒, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝑓⟩)))
16 opeq1 4393 . . . 4 (𝑑 = 𝐷 → ⟨𝑑, 𝑒⟩ = ⟨𝐷, 𝑒⟩)
1716breq2d 4656 . . 3 (𝑑 = 𝐷 → (⟨𝐴, 𝐵⟩Cgr⟨𝑑, 𝑒⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝑒⟩))
18 opeq1 4393 . . . 4 (𝑑 = 𝐷 → ⟨𝑑, 𝑓⟩ = ⟨𝐷, 𝑓⟩)
1918breq2d 4656 . . 3 (𝑑 = 𝐷 → (⟨𝐴, 𝐶⟩Cgr⟨𝑑, 𝑓⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝑓⟩))
2017, 193anbi12d 1398 . 2 (𝑑 = 𝐷 → ((⟨𝐴, 𝐵⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝑒⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝑓⟩)))
21 opeq2 4394 . . . 4 (𝑒 = 𝐸 → ⟨𝐷, 𝑒⟩ = ⟨𝐷, 𝐸⟩)
2221breq2d 4656 . . 3 (𝑒 = 𝐸 → (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝑒⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩))
23 opeq1 4393 . . . 4 (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩)
2423breq2d 4656 . . 3 (𝑒 = 𝐸 → (⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝑓⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝑓⟩))
2522, 243anbi13d 1399 . 2 (𝑒 = 𝐸 → ((⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝑒⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑒, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝑓⟩)))
26 opeq2 4394 . . . 4 (𝑓 = 𝐹 → ⟨𝐷, 𝑓⟩ = ⟨𝐷, 𝐹⟩)
2726breq2d 4656 . . 3 (𝑓 = 𝐹 → (⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝑓⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩))
28 opeq2 4394 . . . 4 (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩)
2928breq2d 4656 . . 3 (𝑓 = 𝐹 → (⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝑓⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝐹⟩))
3027, 293anbi23d 1400 . 2 (𝑓 = 𝐹 → ((⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝑓⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝐹⟩)))
31 fveq2 6178 . 2 (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁))
32 df-cgr3 32123 . 2 Cgr3 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))}
335, 10, 15, 20, 25, 30, 31, 32br6 31622 1 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐷, 𝐸⟩ ∧ ⟨𝐴, 𝐶⟩Cgr⟨𝐷, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐸, 𝐹⟩)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1036   = wceq 1481  wcel 1988  cop 4174   class class class wbr 4644  cfv 5876  cn 11005  𝔼cee 25749  Cgrccgr 25751  Cgr3ccgr3 32118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-iota 5839  df-fv 5884  df-cgr3 32123
This theorem is referenced by:  cgr3permute3  32129  cgr3permute1  32130  cgr3tr4  32134  cgr3com  32135  cgr3rflx  32136  cgrxfr  32137  btwnxfr  32138  lineext  32158  brofs2  32159  brifs2  32160  endofsegid  32167  btwnconn1lem4  32172  btwnconn1lem8  32176  btwnconn1lem11  32179  brsegle2  32191  seglecgr12im  32192  segletr  32196
  Copyright terms: Public domain W3C validator