brcgr3

Description: Binary relation form of the three-place congruence predicate. (Contributed by Scott Fenton, 4-Oct-2013)

		Ref	Expression
	Assertion	brcgr3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨D, ⟨E, F⟩⟩ \leftrightarrow (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))$

Proof

Step	Hyp	Ref	Expression
1		opeq1	$⊢ a = A \to ⟨a, b⟩ = ⟨A, b⟩$
2	1	breq1d	$⊢ a = A \to (⟨a, b⟩ Cgr ⟨d, e⟩ \leftrightarrow ⟨A, b⟩ Cgr ⟨d, e⟩)$
3		opeq1	$⊢ a = A \to ⟨a, c⟩ = ⟨A, c⟩$
4	3	breq1d	$⊢ a = A \to (⟨a, c⟩ Cgr ⟨d, f⟩ \leftrightarrow ⟨A, c⟩ Cgr ⟨d, f⟩)$
5	2 4	3anbi12d	$⊢ a = A \to ((⟨a, b⟩ Cgr ⟨d, e⟩ \land ⟨a, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩) \leftrightarrow (⟨A, b⟩ Cgr ⟨d, e⟩ \land ⟨A, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩))$
6		opeq2	$⊢ b = B \to ⟨A, b⟩ = ⟨A, B⟩$
7	6	breq1d	$⊢ b = B \to (⟨A, b⟩ Cgr ⟨d, e⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨d, e⟩)$
8		opeq1	$⊢ b = B \to ⟨b, c⟩ = ⟨B, c⟩$
9	8	breq1d	$⊢ b = B \to (⟨b, c⟩ Cgr ⟨e, f⟩ \leftrightarrow ⟨B, c⟩ Cgr ⟨e, f⟩)$
10	7 9	3anbi13d	$⊢ b = B \to ((⟨A, b⟩ Cgr ⟨d, e⟩ \land ⟨A, c⟩ Cgr ⟨d, f⟩ \land ⟨b, c⟩ Cgr ⟨e, f⟩) \leftrightarrow (⟨A, B⟩ Cgr ⟨d, e⟩ \land ⟨A, c⟩ Cgr ⟨d, f⟩ \land ⟨B, c⟩ Cgr ⟨e, f⟩))$
11		opeq2	$⊢ c = C \to ⟨A, c⟩ = ⟨A, C⟩$
12	11	breq1d	$⊢ c = C \to (⟨A, c⟩ Cgr ⟨d, f⟩ \leftrightarrow ⟨A, C⟩ Cgr ⟨d, f⟩)$
13		opeq2	$⊢ c = C \to ⟨B, c⟩ = ⟨B, C⟩$
14	13	breq1d	$⊢ c = C \to (⟨B, c⟩ Cgr ⟨e, f⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨e, f⟩)$
15	12 14	3anbi23d	$⊢ c = C \to ((⟨A, B⟩ Cgr ⟨d, e⟩ \land ⟨A, c⟩ Cgr ⟨d, f⟩ \land ⟨B, c⟩ Cgr ⟨e, f⟩) \leftrightarrow (⟨A, B⟩ Cgr ⟨d, e⟩ \land ⟨A, C⟩ Cgr ⟨d, f⟩ \land ⟨B, C⟩ Cgr ⟨e, f⟩))$
16		opeq1	$⊢ d = D \to ⟨d, e⟩ = ⟨D, e⟩$
17	16	breq2d	$⊢ d = D \to (⟨A, B⟩ Cgr ⟨d, e⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨D, e⟩)$
18		opeq1	$⊢ d = D \to ⟨d, f⟩ = ⟨D, f⟩$
19	18	breq2d	$⊢ d = D \to (⟨A, C⟩ Cgr ⟨d, f⟩ \leftrightarrow ⟨A, C⟩ Cgr ⟨D, f⟩)$
20	17 19	3anbi12d	$⊢ d = D \to ((⟨A, B⟩ Cgr ⟨d, e⟩ \land ⟨A, C⟩ Cgr ⟨d, f⟩ \land ⟨B, C⟩ Cgr ⟨e, f⟩) \leftrightarrow (⟨A, B⟩ Cgr ⟨D, e⟩ \land ⟨A, C⟩ Cgr ⟨D, f⟩ \land ⟨B, C⟩ Cgr ⟨e, f⟩))$
21		opeq2	$⊢ e = E \to ⟨D, e⟩ = ⟨D, E⟩$
22	21	breq2d	$⊢ e = E \to (⟨A, B⟩ Cgr ⟨D, e⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨D, E⟩)$
23		opeq1	$⊢ e = E \to ⟨e, f⟩ = ⟨E, f⟩$
24	23	breq2d	$⊢ e = E \to (⟨B, C⟩ Cgr ⟨e, f⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨E, f⟩)$
25	22 24	3anbi13d	$⊢ e = E \to ((⟨A, B⟩ Cgr ⟨D, e⟩ \land ⟨A, C⟩ Cgr ⟨D, f⟩ \land ⟨B, C⟩ Cgr ⟨e, f⟩) \leftrightarrow (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, C⟩ Cgr ⟨D, f⟩ \land ⟨B, C⟩ Cgr ⟨E, f⟩))$
26		opeq2	$⊢ f = F \to ⟨D, f⟩ = ⟨D, F⟩$
27	26	breq2d	$⊢ f = F \to (⟨A, C⟩ Cgr ⟨D, f⟩ \leftrightarrow ⟨A, C⟩ Cgr ⟨D, F⟩)$
28		opeq2	$⊢ f = F \to ⟨E, f⟩ = ⟨E, F⟩$
29	28	breq2d	$⊢ f = F \to (⟨B, C⟩ Cgr ⟨E, f⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨E, F⟩)$
30	27 29	3anbi23d	$⊢ f = F \to ((⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, C⟩ Cgr ⟨D, f⟩ \land ⟨B, C⟩ Cgr ⟨E, f⟩) \leftrightarrow (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))$
31		fveq2	$⊢ n = N \to 𝔼 (n) = 𝔼 (N)$
32		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⟩))\}$
33	5 10 15 20 25 30 31 32	br6	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨A, ⟨B, C⟩⟩ Cgr3 ⟨D, ⟨E, F⟩⟩ \leftrightarrow (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨A, C⟩ Cgr ⟨D, F⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩))$

Metamath Proof Explorer

Theorem brcgr3

Proof