Definition df-cgr3 35013

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

Step	Hyp	Ref	Expression
1		ccgr3 35008	. 2 class Cgr3
2		vp	. . . . . . . . . . . . 13 setvar 𝑝
3	2	cv 1541	. . . . . . . . . . . 12 class 𝑝
4		va	. . . . . . . . . . . . . 14 setvar 𝑎
5	4	cv 1541	. . . . . . . . . . . . 13 class 𝑎
6		vb	. . . . . . . . . . . . . . 15 setvar 𝑏
7	6	cv 1541	. . . . . . . . . . . . . 14 class 𝑏
8		vc	. . . . . . . . . . . . . . 15 setvar 𝑐
9	8	cv 1541	. . . . . . . . . . . . . 14 class 𝑐
10	7, 9	cop 4635	. . . . . . . . . . . . 13 class ⟨𝑏, 𝑐⟩
11	5, 10	cop 4635	. . . . . . . . . . . 12 class ⟨𝑎, ⟨𝑏, 𝑐⟩⟩
12	3, 11	wceq 1542	. . . . . . . . . . 11 wff 𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩
13		vq	. . . . . . . . . . . . 13 setvar 𝑞
14	13	cv 1541	. . . . . . . . . . . 12 class 𝑞
15		vd	. . . . . . . . . . . . . 14 setvar 𝑑
16	15	cv 1541	. . . . . . . . . . . . 13 class 𝑑
17		ve	. . . . . . . . . . . . . . 15 setvar 𝑒
18	17	cv 1541	. . . . . . . . . . . . . 14 class 𝑒
19		vf	. . . . . . . . . . . . . . 15 setvar 𝑓
20	19	cv 1541	. . . . . . . . . . . . . 14 class 𝑓
21	18, 20	cop 4635	. . . . . . . . . . . . 13 class ⟨𝑒, 𝑓⟩
22	16, 21	cop 4635	. . . . . . . . . . . 12 class ⟨𝑑, ⟨𝑒, 𝑓⟩⟩
23	14, 22	wceq 1542	. . . . . . . . . . 11 wff 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩
24	5, 7	cop 4635	. . . . . . . . . . . . 13 class ⟨𝑎, 𝑏⟩
25	16, 18	cop 4635	. . . . . . . . . . . . 13 class ⟨𝑑, 𝑒⟩
26		ccgr 28148	. . . . . . . . . . . . 13 class Cgr
27	24, 25, 26	wbr 5149	. . . . . . . . . . . 12 wff ⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩
28	5, 9	cop 4635	. . . . . . . . . . . . 13 class ⟨𝑎, 𝑐⟩
29	16, 20	cop 4635	. . . . . . . . . . . . 13 class ⟨𝑑, 𝑓⟩
30	28, 29, 26	wbr 5149	. . . . . . . . . . . 12 wff ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩
31	10, 21, 26	wbr 5149	. . . . . . . . . . . 12 wff ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩
32	27, 30, 31	w3a 1088	. . . . . . . . . . 11 wff (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩)
33	12, 23, 32	w3a 1088	. . . . . . . . . 10 wff (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
34		vn	. . . . . . . . . . . 12 setvar 𝑛
35	34	cv 1541	. . . . . . . . . . 11 class 𝑛
36		cee 28146	. . . . . . . . . . 11 class 𝔼
37	35, 36	cfv 6544	. . . . . . . . . 10 class (𝔼‘𝑛)
38	33, 19, 37	wrex 3071	. . . . . . . . 9 wff ∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
39	38, 17, 37	wrex 3071	. . . . . . . 8 wff ∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
40	39, 15, 37	wrex 3071	. . . . . . 7 wff ∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
41	40, 8, 37	wrex 3071	. . . . . 6 wff ∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
42	41, 6, 37	wrex 3071	. . . . 5 wff ∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
43	42, 4, 37	wrex 3071	. . . 4 wff ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
44		cn 12212	. . . 4 class ℕ
45	43, 34, 44	wrex 3071	. . 3 wff ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))
46	45, 2, 13	copab 5211	. 2 class {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))}
47	1, 46	wceq 1542	1 wff Cgr3 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑑, 𝑒⟩ ∧ ⟨𝑎, 𝑐⟩Cgr⟨𝑑, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑒, 𝑓⟩))}

This definition is referenced by:  brcgr3  35018