brifs

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

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

Metamath Proof Explorer

Theorem brifs

Proof