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 = \{⟨p, q⟩ \| \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists e \in 𝔼 (n) \exists f \in 𝔼 (n) (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land (⟨a, b⟩ Cgr ⟨d, e⟩ \land ⟨a, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccgr3	$class Cgr3$
1		vp	$setvar p$
2		vq	$setvar q$
3		vn	$setvar n$
4		cn	$class ℕ$
5		va	$setvar a$
6		cee	$class 𝔼$
7	3	cv	$setvar n$
8	7 6	cfv	$class 𝔼 (n)$
9		vb	$setvar b$
10		vc	$setvar c$
11		vd	$setvar d$
12		ve	$setvar e$
13		vf	$setvar f$
14	1	cv	$setvar p$
15	5	cv	$setvar a$
16	9	cv	$setvar b$
17	10	cv	$setvar c$
18	16 17	cop	$class ⟨b, c⟩$
19	15 18	cop	$class ⟨a, ⟨b, c⟩⟩$
20	14 19	wceq	$wff p = ⟨a, ⟨b, c⟩⟩$
21	2	cv	$setvar q$
22	11	cv	$setvar d$
23	12	cv	$setvar e$
24	13	cv	$setvar f$
25	23 24	cop	$class ⟨e, f⟩$
26	22 25	cop	$class ⟨d, ⟨e, f⟩⟩$
27	21 26	wceq	$wff q = ⟨d, ⟨e, f⟩⟩$
28	15 16	cop	$class ⟨a, b⟩$
29		ccgr	$class Cgr$
30	22 23	cop	$class ⟨d, e⟩$
31	28 30 29	wbr	$wff ⟨a, b⟩ Cgr ⟨d, e⟩$
32	15 17	cop	$class ⟨a, c⟩$
33	22 24	cop	$class ⟨d, f⟩$
34	32 33 29	wbr	$wff ⟨a, c⟩ Cgr ⟨d, f⟩$
35	18 25 29	wbr	$wff ⟨b, c⟩ Cgr ⟨e, f⟩$
36	31 34 35	w3a	$wff (⟨a, b⟩ Cgr ⟨d, e⟩ \land ⟨a, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩)$
37	20 27 36	w3a	$wff (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land (⟨a, b⟩ Cgr ⟨d, e⟩ \land ⟨a, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩))$
38	37 13 8	wrex	$wff \exists f \in 𝔼 (n) (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land (⟨a, b⟩ Cgr ⟨d, e⟩ \land ⟨a, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩))$
39	38 12 8	wrex	$wff \exists e \in 𝔼 (n) \exists f \in 𝔼 (n) (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land (⟨a, b⟩ Cgr ⟨d, e⟩ \land ⟨a, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩))$
40	39 11 8	wrex	$wff \exists d \in 𝔼 (n) \exists e \in 𝔼 (n) \exists f \in 𝔼 (n) (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land (⟨a, b⟩ Cgr ⟨d, e⟩ \land ⟨a, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩))$
41	40 10 8	wrex	$wff \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists e \in 𝔼 (n) \exists f \in 𝔼 (n) (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land (⟨a, b⟩ Cgr ⟨d, e⟩ \land ⟨a, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩))$
42	41 9 8	wrex	$wff \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists e \in 𝔼 (n) \exists f \in 𝔼 (n) (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land (⟨a, b⟩ Cgr ⟨d, e⟩ \land ⟨a, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩))$
43	42 5 8	wrex	$wff \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists e \in 𝔼 (n) \exists f \in 𝔼 (n) (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land (⟨a, b⟩ Cgr ⟨d, e⟩ \land ⟨a, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩))$
44	43 3 4	wrex	$wff \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists e \in 𝔼 (n) \exists f \in 𝔼 (n) (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land (⟨a, b⟩ Cgr ⟨d, e⟩ \land ⟨a, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩))$
45	44 1 2	copab	$class \{⟨p, q⟩ \| \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists e \in 𝔼 (n) \exists f \in 𝔼 (n) (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land (⟨a, b⟩ Cgr ⟨d, e⟩ \land ⟨a, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩))\}$
46	0 45	wceq	$wff Cgr3 = \{⟨p, q⟩ \| \exists n \in ℕ \exists a \in 𝔼 (n) \exists b \in 𝔼 (n) \exists c \in 𝔼 (n) \exists d \in 𝔼 (n) \exists e \in 𝔼 (n) \exists f \in 𝔼 (n) (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land (⟨a, b⟩ Cgr ⟨d, e⟩ \land ⟨a, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩))\}$

Metamath Proof Explorer

Definition df-cgr3

Detailed syntax breakdown