brofs

Description: Binary relation form of the outer five segment predicate. (Contributed by Scott Fenton, 21-Sep-2013)

		Ref	Expression
	Assertion	brofs	$⊢ ((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) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$

Proof

Step	Hyp	Ref	Expression
1		opeq1	$⊢ a = A \to ⟨a, c⟩ = ⟨A, c⟩$
2	1	breq2d	$⊢ a = A \to (b Btwn ⟨a, c⟩ \leftrightarrow b Btwn ⟨A, c⟩)$
3	2	anbi1d	$⊢ a = A \to ((b Btwn ⟨a, c⟩ \land f Btwn ⟨e, g⟩) \leftrightarrow (b Btwn ⟨A, c⟩ \land f Btwn ⟨e, g⟩))$
4		opeq1	$⊢ a = A \to ⟨a, b⟩ = ⟨A, b⟩$
5	4	breq1d	$⊢ a = A \to (⟨a, b⟩ Cgr ⟨e, f⟩ \leftrightarrow ⟨A, b⟩ Cgr ⟨e, f⟩)$
6	5	anbi1d	$⊢ a = A \to ((⟨a, b⟩ Cgr ⟨e, f⟩ \land ⟨b, c⟩ Cgr ⟨f, g⟩) \leftrightarrow (⟨A, b⟩ Cgr ⟨e, f⟩ \land ⟨b, c⟩ Cgr ⟨f, g⟩))$
7		opeq1	$⊢ a = A \to ⟨a, d⟩ = ⟨A, d⟩$
8	7	breq1d	$⊢ a = A \to (⟨a, d⟩ Cgr ⟨e, h⟩ \leftrightarrow ⟨A, d⟩ Cgr ⟨e, h⟩)$
9	8	anbi1d	$⊢ a = A \to ((⟨a, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩) \leftrightarrow (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩))$
10	3 6 9	3anbi123d	$⊢ a = A \to (((b Btwn ⟨a, c⟩ \land f Btwn ⟨e, g⟩) \land (⟨a, b⟩ Cgr ⟨e, f⟩ \land ⟨b, c⟩ Cgr ⟨f, g⟩) \land (⟨a, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩)) \leftrightarrow ((b Btwn ⟨A, c⟩ \land f Btwn ⟨e, g⟩) \land (⟨A, b⟩ Cgr ⟨e, f⟩ \land ⟨b, c⟩ Cgr ⟨f, g⟩) \land (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩)))$
11		breq1	$⊢ b = B \to (b Btwn ⟨A, c⟩ \leftrightarrow B Btwn ⟨A, c⟩)$
12	11	anbi1d	$⊢ b = B \to ((b Btwn ⟨A, c⟩ \land f Btwn ⟨e, g⟩) \leftrightarrow (B Btwn ⟨A, c⟩ \land f Btwn ⟨e, g⟩))$
13		opeq2	$⊢ b = B \to ⟨A, b⟩ = ⟨A, B⟩$
14	13	breq1d	$⊢ b = B \to (⟨A, b⟩ Cgr ⟨e, f⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨e, f⟩)$
15		opeq1	$⊢ b = B \to ⟨b, c⟩ = ⟨B, c⟩$
16	15	breq1d	$⊢ b = B \to (⟨b, c⟩ Cgr ⟨f, g⟩ \leftrightarrow ⟨B, c⟩ Cgr ⟨f, g⟩)$
17	14 16	anbi12d	$⊢ b = B \to ((⟨A, b⟩ Cgr ⟨e, f⟩ \land ⟨b, c⟩ Cgr ⟨f, g⟩) \leftrightarrow (⟨A, B⟩ Cgr ⟨e, f⟩ \land ⟨B, c⟩ Cgr ⟨f, g⟩))$
18		opeq1	$⊢ b = B \to ⟨b, d⟩ = ⟨B, d⟩$
19	18	breq1d	$⊢ b = B \to (⟨b, d⟩ Cgr ⟨f, h⟩ \leftrightarrow ⟨B, d⟩ Cgr ⟨f, h⟩)$
20	19	anbi2d	$⊢ b = B \to ((⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩) \leftrightarrow (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨B, d⟩ Cgr ⟨f, h⟩))$
21	12 17 20	3anbi123d	$⊢ b = B \to (((b Btwn ⟨A, c⟩ \land f Btwn ⟨e, g⟩) \land (⟨A, b⟩ Cgr ⟨e, f⟩ \land ⟨b, c⟩ Cgr ⟨f, g⟩) \land (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩)) \leftrightarrow ((B Btwn ⟨A, c⟩ \land f Btwn ⟨e, g⟩) \land (⟨A, B⟩ Cgr ⟨e, f⟩ \land ⟨B, c⟩ Cgr ⟨f, g⟩) \land (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨B, d⟩ Cgr ⟨f, h⟩)))$
22		opeq2	$⊢ c = C \to ⟨A, c⟩ = ⟨A, C⟩$
23	22	breq2d	$⊢ c = C \to (B Btwn ⟨A, c⟩ \leftrightarrow B Btwn ⟨A, C⟩)$
24	23	anbi1d	$⊢ c = C \to ((B Btwn ⟨A, c⟩ \land f Btwn ⟨e, g⟩) \leftrightarrow (B Btwn ⟨A, C⟩ \land f Btwn ⟨e, g⟩))$
25		opeq2	$⊢ c = C \to ⟨B, c⟩ = ⟨B, C⟩$
26	25	breq1d	$⊢ c = C \to (⟨B, c⟩ Cgr ⟨f, g⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨f, g⟩)$
27	26	anbi2d	$⊢ c = C \to ((⟨A, B⟩ Cgr ⟨e, f⟩ \land ⟨B, c⟩ Cgr ⟨f, g⟩) \leftrightarrow (⟨A, B⟩ Cgr ⟨e, f⟩ \land ⟨B, C⟩ Cgr ⟨f, g⟩))$
28	24 27	3anbi12d	$⊢ c = C \to (((B Btwn ⟨A, c⟩ \land f Btwn ⟨e, g⟩) \land (⟨A, B⟩ Cgr ⟨e, f⟩ \land ⟨B, c⟩ Cgr ⟨f, g⟩) \land (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨B, d⟩ Cgr ⟨f, h⟩)) \leftrightarrow ((B Btwn ⟨A, C⟩ \land f Btwn ⟨e, g⟩) \land (⟨A, B⟩ Cgr ⟨e, f⟩ \land ⟨B, C⟩ Cgr ⟨f, g⟩) \land (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨B, d⟩ Cgr ⟨f, h⟩)))$
29		opeq2	$⊢ d = D \to ⟨A, d⟩ = ⟨A, D⟩$
30	29	breq1d	$⊢ d = D \to (⟨A, d⟩ Cgr ⟨e, h⟩ \leftrightarrow ⟨A, D⟩ Cgr ⟨e, h⟩)$
31		opeq2	$⊢ d = D \to ⟨B, d⟩ = ⟨B, D⟩$
32	31	breq1d	$⊢ d = D \to (⟨B, d⟩ Cgr ⟨f, h⟩ \leftrightarrow ⟨B, D⟩ Cgr ⟨f, h⟩)$
33	30 32	anbi12d	$⊢ d = D \to ((⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨B, d⟩ Cgr ⟨f, h⟩) \leftrightarrow (⟨A, D⟩ Cgr ⟨e, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩))$
34	33	3anbi3d	$⊢ d = D \to (((B Btwn ⟨A, C⟩ \land f Btwn ⟨e, g⟩) \land (⟨A, B⟩ Cgr ⟨e, f⟩ \land ⟨B, C⟩ Cgr ⟨f, g⟩) \land (⟨A, d⟩ Cgr ⟨e, h⟩ \land ⟨B, d⟩ Cgr ⟨f, h⟩)) \leftrightarrow ((B Btwn ⟨A, C⟩ \land f Btwn ⟨e, g⟩) \land (⟨A, B⟩ Cgr ⟨e, f⟩ \land ⟨B, C⟩ Cgr ⟨f, g⟩) \land (⟨A, D⟩ Cgr ⟨e, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩)))$
35		opeq1	$⊢ e = E \to ⟨e, g⟩ = ⟨E, g⟩$
36	35	breq2d	$⊢ e = E \to (f Btwn ⟨e, g⟩ \leftrightarrow f Btwn ⟨E, g⟩)$
37	36	anbi2d	$⊢ e = E \to ((B Btwn ⟨A, C⟩ \land f Btwn ⟨e, g⟩) \leftrightarrow (B Btwn ⟨A, C⟩ \land f Btwn ⟨E, g⟩))$
38		opeq1	$⊢ e = E \to ⟨e, f⟩ = ⟨E, f⟩$
39	38	breq2d	$⊢ e = E \to (⟨A, B⟩ Cgr ⟨e, f⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨E, f⟩)$
40	39	anbi1d	$⊢ e = E \to ((⟨A, B⟩ Cgr ⟨e, f⟩ \land ⟨B, C⟩ Cgr ⟨f, g⟩) \leftrightarrow (⟨A, B⟩ Cgr ⟨E, f⟩ \land ⟨B, C⟩ Cgr ⟨f, g⟩))$
41		opeq1	$⊢ e = E \to ⟨e, h⟩ = ⟨E, h⟩$
42	41	breq2d	$⊢ e = E \to (⟨A, D⟩ Cgr ⟨e, h⟩ \leftrightarrow ⟨A, D⟩ Cgr ⟨E, h⟩)$
43	42	anbi1d	$⊢ e = E \to ((⟨A, D⟩ Cgr ⟨e, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩) \leftrightarrow (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩))$
44	37 40 43	3anbi123d	$⊢ e = E \to (((B Btwn ⟨A, C⟩ \land f Btwn ⟨e, g⟩) \land (⟨A, B⟩ Cgr ⟨e, f⟩ \land ⟨B, C⟩ Cgr ⟨f, g⟩) \land (⟨A, D⟩ Cgr ⟨e, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩)) \leftrightarrow ((B Btwn ⟨A, C⟩ \land f Btwn ⟨E, g⟩) \land (⟨A, B⟩ Cgr ⟨E, f⟩ \land ⟨B, C⟩ Cgr ⟨f, g⟩) \land (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩)))$
45		breq1	$⊢ f = F \to (f Btwn ⟨E, g⟩ \leftrightarrow F Btwn ⟨E, g⟩)$
46	45	anbi2d	$⊢ f = F \to ((B Btwn ⟨A, C⟩ \land f Btwn ⟨E, g⟩) \leftrightarrow (B Btwn ⟨A, C⟩ \land F Btwn ⟨E, g⟩))$
47		opeq2	$⊢ f = F \to ⟨E, f⟩ = ⟨E, F⟩$
48	47	breq2d	$⊢ f = F \to (⟨A, B⟩ Cgr ⟨E, f⟩ \leftrightarrow ⟨A, B⟩ Cgr ⟨E, F⟩)$
49		opeq1	$⊢ f = F \to ⟨f, g⟩ = ⟨F, g⟩$
50	49	breq2d	$⊢ f = F \to (⟨B, C⟩ Cgr ⟨f, g⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨F, g⟩)$
51	48 50	anbi12d	$⊢ f = F \to ((⟨A, B⟩ Cgr ⟨E, f⟩ \land ⟨B, C⟩ Cgr ⟨f, g⟩) \leftrightarrow (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, g⟩))$
52		opeq1	$⊢ f = F \to ⟨f, h⟩ = ⟨F, h⟩$
53	52	breq2d	$⊢ f = F \to (⟨B, D⟩ Cgr ⟨f, h⟩ \leftrightarrow ⟨B, D⟩ Cgr ⟨F, h⟩)$
54	53	anbi2d	$⊢ f = F \to ((⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩) \leftrightarrow (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨F, h⟩))$
55	46 51 54	3anbi123d	$⊢ f = F \to (((B Btwn ⟨A, C⟩ \land f Btwn ⟨E, g⟩) \land (⟨A, B⟩ Cgr ⟨E, f⟩ \land ⟨B, C⟩ Cgr ⟨f, g⟩) \land (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨f, h⟩)) \leftrightarrow ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, g⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, g⟩) \land (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨F, h⟩)))$
56		opeq2	$⊢ g = G \to ⟨E, g⟩ = ⟨E, G⟩$
57	56	breq2d	$⊢ g = G \to (F Btwn ⟨E, g⟩ \leftrightarrow F Btwn ⟨E, G⟩)$
58	57	anbi2d	$⊢ g = G \to ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, g⟩) \leftrightarrow (B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩))$
59		opeq2	$⊢ g = G \to ⟨F, g⟩ = ⟨F, G⟩$
60	59	breq2d	$⊢ g = G \to (⟨B, C⟩ Cgr ⟨F, g⟩ \leftrightarrow ⟨B, C⟩ Cgr ⟨F, G⟩)$
61	60	anbi2d	$⊢ g = G \to ((⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, g⟩) \leftrightarrow (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩))$
62	58 61	3anbi12d	$⊢ g = G \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, g⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, g⟩) \land (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨F, h⟩)) \leftrightarrow ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨F, h⟩)))$
63		opeq2	$⊢ h = H \to ⟨E, h⟩ = ⟨E, H⟩$
64	63	breq2d	$⊢ h = H \to (⟨A, D⟩ Cgr ⟨E, h⟩ \leftrightarrow ⟨A, D⟩ Cgr ⟨E, H⟩)$
65		opeq2	$⊢ h = H \to ⟨F, h⟩ = ⟨F, H⟩$
66	65	breq2d	$⊢ h = H \to (⟨B, D⟩ Cgr ⟨F, h⟩ \leftrightarrow ⟨B, D⟩ Cgr ⟨F, H⟩)$
67	64 66	anbi12d	$⊢ h = H \to ((⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨F, h⟩) \leftrightarrow (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩))$
68	67	3anbi3d	$⊢ h = H \to (((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, h⟩ \land ⟨B, D⟩ Cgr ⟨F, h⟩)) \leftrightarrow ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$
69		fveq2	$⊢ n = N \to 𝔼 (n) = 𝔼 (N)$
70		df-ofs	$⊢ OuterFiveSeg = \{⟨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) \exists g \in 𝔼 (n) \exists h \in 𝔼 (n) (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ((b Btwn ⟨a, c⟩ \land f Btwn ⟨e, g⟩) \land (⟨a, b⟩ Cgr ⟨e, f⟩ \land ⟨b, c⟩ Cgr ⟨f, g⟩) \land (⟨a, d⟩ Cgr ⟨e, h⟩ \land ⟨b, d⟩ Cgr ⟨f, h⟩)))\}$
71	10 21 28 34 44 55 62 68 69 70	br8	$⊢ ((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) \land G \in 𝔼 (N) \land H \in 𝔼 (N))) \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ OuterFiveSeg ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow ((B Btwn ⟨A, C⟩ \land F Btwn ⟨E, G⟩) \land (⟨A, B⟩ Cgr ⟨E, F⟩ \land ⟨B, C⟩ Cgr ⟨F, G⟩) \land (⟨A, D⟩ Cgr ⟨E, H⟩ \land ⟨B, D⟩ Cgr ⟨F, H⟩)))$

Metamath Proof Explorer

Theorem brofs

Proof