Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cgr3 Structured version   Visualization version   GIF version

Definition df-cgr3 32273
 Description: The three place congruence predicate. This is an abbreviation for saying that all three pair in a triple are congruent with each other. Three place form of Definition 4.4 of [Schwabhauser] p. 35. (Contributed by Scott Fenton, 4-Oct-2013.)
Assertion
Ref Expression
df-cgr3 Cgr3 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))}
Distinct variable group:   𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑛,𝑝,𝑞

Detailed syntax breakdown of Definition df-cgr3
StepHypRef Expression
1 ccgr3 32268 . 2 class Cgr3
2 vp . . . . . . . . . . . . 13 setvar 𝑝
32cv 1522 . . . . . . . . . . . 12 class 𝑝
4 va . . . . . . . . . . . . . 14 setvar 𝑎
54cv 1522 . . . . . . . . . . . . 13 class 𝑎
6 vb . . . . . . . . . . . . . . 15 setvar 𝑏
76cv 1522 . . . . . . . . . . . . . 14 class 𝑏
8 vc . . . . . . . . . . . . . . 15 setvar 𝑐
98cv 1522 . . . . . . . . . . . . . 14 class 𝑐
107, 9cop 4216 . . . . . . . . . . . . 13 class 𝑏, 𝑐
115, 10cop 4216 . . . . . . . . . . . 12 class 𝑎, ⟨𝑏, 𝑐⟩⟩
123, 11wceq 1523 . . . . . . . . . . 11 wff 𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩
13 vq . . . . . . . . . . . . 13 setvar 𝑞
1413cv 1522 . . . . . . . . . . . 12 class 𝑞
15 vd . . . . . . . . . . . . . 14 setvar 𝑑
1615cv 1522 . . . . . . . . . . . . 13 class 𝑑
17 ve . . . . . . . . . . . . . . 15 setvar 𝑒
1817cv 1522 . . . . . . . . . . . . . 14 class 𝑒
19 vf . . . . . . . . . . . . . . 15 setvar 𝑓
2019cv 1522 . . . . . . . . . . . . . 14 class 𝑓
2118, 20cop 4216 . . . . . . . . . . . . 13 class 𝑒, 𝑓
2216, 21cop 4216 . . . . . . . . . . . 12 class 𝑑, ⟨𝑒, 𝑓⟩⟩
2314, 22wceq 1523 . . . . . . . . . . 11 wff 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩
245, 7cop 4216 . . . . . . . . . . . . 13 class 𝑎, 𝑏
2516, 18cop 4216 . . . . . . . . . . . . 13 class 𝑑, 𝑒
26 ccgr 25815 . . . . . . . . . . . . 13 class Cgr
2724, 25, 26wbr 4685 . . . . . . . . . . . 12 wff 𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒
285, 9cop 4216 . . . . . . . . . . . . 13 class 𝑎, 𝑐
2916, 20cop 4216 . . . . . . . . . . . . 13 class 𝑑, 𝑓
3028, 29, 26wbr 4685 . . . . . . . . . . . 12 wff 𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓
3110, 21, 26wbr 4685 . . . . . . . . . . . 12 wff 𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓
3227, 30, 31w3a 1054 . . . . . . . . . . 11 wff (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩)
3312, 23, 32w3a 1054 . . . . . . . . . 10 wff (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
34 vn . . . . . . . . . . . 12 setvar 𝑛
3534cv 1522 . . . . . . . . . . 11 class 𝑛
36 cee 25813 . . . . . . . . . . 11 class 𝔼
3735, 36cfv 5926 . . . . . . . . . 10 class (𝔼‘𝑛)
3833, 19, 37wrex 2942 . . . . . . . . 9 wff 𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
3938, 17, 37wrex 2942 . . . . . . . 8 wff 𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
4039, 15, 37wrex 2942 . . . . . . 7 wff 𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
4140, 8, 37wrex 2942 . . . . . 6 wff 𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
4241, 6, 37wrex 2942 . . . . 5 wff 𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
4342, 4, 37wrex 2942 . . . 4 wff 𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
44 cn 11058 . . . 4 class
4543, 34, 44wrex 2942 . . 3 wff 𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
4645, 2, 13copab 4745 . 2 class {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))}
471, 46wceq 1523 1 wff Cgr3 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))}
 Colors of variables: wff setvar class This definition is referenced by:  brcgr3  32278
 Copyright terms: Public domain W3C validator