Definition df-cgr3

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)

	Ref	Expression
Assertion	df-cgr3	⊢ Cgr3 = { ⟨ 𝑝 , 𝑞 ⟩ ∣ ∃ 𝑛 ∈ ℕ ∃ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑑 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑒 ∈ ( 𝔼 ‘ 𝑛 ) ∃ 𝑓 ∈ ( 𝔼 ‘ 𝑛 ) ( 𝑝 = ⟨ 𝑎 , ⟨ 𝑏 , 𝑐 ⟩ ⟩ ∧ 𝑞 = ⟨ 𝑑 , ⟨ 𝑒 , 𝑓 ⟩ ⟩ ∧ ( ⟨ 𝑎 , 𝑏 ⟩ Cgr ⟨ 𝑑 , 𝑒 ⟩ ∧ ⟨ 𝑎 , 𝑐 ⟩ Cgr ⟨ 𝑑 , 𝑓 ⟩ ∧ ⟨ 𝑏 , 𝑐 ⟩ Cgr ⟨ 𝑒 , 𝑓 ⟩ ) ) }

Detailed syntax breakdown

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