Theorem brifs 33975

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

Assertion

Ref	Expression
brifs	⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ InnerFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))

Proof of Theorem brifs

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 ℎ 𝑝 𝑞 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opeq1 4756	. . . . 5 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑐⟩ = ⟨𝐴, 𝑐⟩)
2	1	breq2d 5039	. . . 4 ⊢ (𝑎 = 𝐴 → (𝑏 Btwn ⟨𝑎, 𝑐⟩ ↔ 𝑏 Btwn ⟨𝐴, 𝑐⟩))
3	2	anbi1d 633	. . 3 ⊢ (𝑎 = 𝐴 → ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
4	1	breq1d 5037	. . . 4 ⊢ (𝑎 = 𝐴 → (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩))
5	4	anbi1d 633	. . 3 ⊢ (𝑎 = 𝐴 → ((⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
6		opeq1 4756	. . . . 5 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑑⟩ = ⟨𝐴, 𝑑⟩)
7	6	breq1d 5037	. . . 4 ⊢ (𝑎 = 𝐴 → (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ↔ ⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩))
8	7	anbi1d 633	. . 3 ⊢ (𝑎 = 𝐴 → ((⟨𝑎, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩)))
9	3, 5, 8	3anbi123d 1437	. 2 ⊢ (𝑎 = 𝐴 → (((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩))))
10		breq1 5030	. . . 4 ⊢ (𝑏 = 𝐵 → (𝑏 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝑐⟩))
11	10	anbi1d 633	. . 3 ⊢ (𝑏 = 𝐵 → ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
12		opeq1 4756	. . . . 5 ⊢ (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
13	12	breq1d 5037	. . . 4 ⊢ (𝑏 = 𝐵 → (⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩))
14	13	anbi2d 632	. . 3 ⊢ (𝑏 = 𝐵 → ((⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
15	11, 14	3anbi12d 1438	. 2 ⊢ (𝑏 = 𝐵 → (((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩))))
16		opeq2 4758	. . . . 5 ⊢ (𝑐 = 𝐶 → ⟨𝐴, 𝑐⟩ = ⟨𝐴, 𝐶⟩)
17	16	breq2d 5039	. . . 4 ⊢ (𝑐 = 𝐶 → (𝐵 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝐶⟩))
18	17	anbi1d 633	. . 3 ⊢ (𝑐 = 𝐶 → ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
19	16	breq1d 5037	. . . 4 ⊢ (𝑐 = 𝐶 → (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩))
20		opeq2 4758	. . . . 5 ⊢ (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
21	20	breq1d 5037	. . . 4 ⊢ (𝑐 = 𝐶 → (⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩))
22	19, 21	anbi12d 634	. . 3 ⊢ (𝑐 = 𝐶 → ((⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
23		opeq1 4756	. . . . 5 ⊢ (𝑐 = 𝐶 → ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝑑⟩)
24	23	breq1d 5037	. . . 4 ⊢ (𝑐 = 𝐶 → (⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩ ↔ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ℎ⟩))
25	24	anbi2d 632	. . 3 ⊢ (𝑐 = 𝐶 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ℎ⟩)))
26	18, 22, 25	3anbi123d 1437	. 2 ⊢ (𝑐 = 𝐶 → (((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ℎ⟩))))
27		opeq2 4758	. . . . 5 ⊢ (𝑑 = 𝐷 → ⟨𝐴, 𝑑⟩ = ⟨𝐴, 𝐷⟩)
28	27	breq1d 5037	. . . 4 ⊢ (𝑑 = 𝐷 → (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩))
29		opeq2 4758	. . . . 5 ⊢ (𝑑 = 𝐷 → ⟨𝐶, 𝑑⟩ = ⟨𝐶, 𝐷⟩)
30	29	breq1d 5037	. . . 4 ⊢ (𝑑 = 𝐷 → (⟨𝐶, 𝑑⟩Cgr⟨𝑔, ℎ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩))
31	28, 30	anbi12d 634	. . 3 ⊢ (𝑑 = 𝐷 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ℎ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩)))
32	31	3anbi3d 1443	. 2 ⊢ (𝑑 = 𝐷 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩))))
33		opeq1 4756	. . . . 5 ⊢ (𝑒 = 𝐸 → ⟨𝑒, 𝑔⟩ = ⟨𝐸, 𝑔⟩)
34	33	breq2d 5039	. . . 4 ⊢ (𝑒 = 𝐸 → (𝑓 Btwn ⟨𝑒, 𝑔⟩ ↔ 𝑓 Btwn ⟨𝐸, 𝑔⟩))
35	34	anbi2d 632	. . 3 ⊢ (𝑒 = 𝐸 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩)))
36	33	breq2d 5039	. . . 4 ⊢ (𝑒 = 𝐸 → (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩))
37	36	anbi1d 633	. . 3 ⊢ (𝑒 = 𝐸 → ((⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
38		opeq1 4756	. . . . 5 ⊢ (𝑒 = 𝐸 → ⟨𝑒, ℎ⟩ = ⟨𝐸, ℎ⟩)
39	38	breq2d 5039	. . . 4 ⊢ (𝑒 = 𝐸 → (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩))
40	39	anbi1d 633	. . 3 ⊢ (𝑒 = 𝐸 → ((⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩)))
41	35, 37, 40	3anbi123d 1437	. 2 ⊢ (𝑒 = 𝐸 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩))))
42		breq1 5030	. . . 4 ⊢ (𝑓 = 𝐹 → (𝑓 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝑔⟩))
43	42	anbi2d 632	. . 3 ⊢ (𝑓 = 𝐹 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩)))
44		opeq1 4756	. . . . 5 ⊢ (𝑓 = 𝐹 → ⟨𝑓, 𝑔⟩ = ⟨𝐹, 𝑔⟩)
45	44	breq2d 5039	. . . 4 ⊢ (𝑓 = 𝐹 → (⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩))
46	45	anbi2d 632	. . 3 ⊢ (𝑓 = 𝐹 → ((⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩)))
47	43, 46	3anbi12d 1438	. 2 ⊢ (𝑓 = 𝐹 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩))))
48		opeq2 4758	. . . . 5 ⊢ (𝑔 = 𝐺 → ⟨𝐸, 𝑔⟩ = ⟨𝐸, 𝐺⟩)
49	48	breq2d 5039	. . . 4 ⊢ (𝑔 = 𝐺 → (𝐹 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝐺⟩))
50	49	anbi2d 632	. . 3 ⊢ (𝑔 = 𝐺 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩)))
51	48	breq2d 5039	. . . 4 ⊢ (𝑔 = 𝐺 → (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩))
52		opeq2 4758	. . . . 5 ⊢ (𝑔 = 𝐺 → ⟨𝐹, 𝑔⟩ = ⟨𝐹, 𝐺⟩)
53	52	breq2d 5039	. . . 4 ⊢ (𝑔 = 𝐺 → (⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩))
54	51, 53	anbi12d 634	. . 3 ⊢ (𝑔 = 𝐺 → ((⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)))
55		opeq1 4756	. . . . 5 ⊢ (𝑔 = 𝐺 → ⟨𝑔, ℎ⟩ = ⟨𝐺, ℎ⟩)
56	55	breq2d 5039	. . . 4 ⊢ (𝑔 = 𝐺 → (⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ℎ⟩))
57	56	anbi2d 632	. . 3 ⊢ (𝑔 = 𝐺 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ℎ⟩)))
58	50, 54, 57	3anbi123d 1437	. 2 ⊢ (𝑔 = 𝐺 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ℎ⟩))))
59		opeq2 4758	. . . . 5 ⊢ (ℎ = 𝐻 → ⟨𝐸, ℎ⟩ = ⟨𝐸, 𝐻⟩)
60	59	breq2d 5039	. . . 4 ⊢ (ℎ = 𝐻 → (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩))
61		opeq2 4758	. . . . 5 ⊢ (ℎ = 𝐻 → ⟨𝐺, ℎ⟩ = ⟨𝐺, 𝐻⟩)
62	61	breq2d 5039	. . . 4 ⊢ (ℎ = 𝐻 → (⟨𝐶, 𝐷⟩Cgr⟨𝐺, ℎ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
63	60, 62	anbi12d 634	. . 3 ⊢ (ℎ = 𝐻 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ℎ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
64	63	3anbi3d 1443	. 2 ⊢ (ℎ = 𝐻 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
65		fveq2 6668	. 2 ⊢ (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁))
66		df-ifs 33972	. 2 ⊢ InnerFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)∃𝑔 ∈ (𝔼‘𝑛)∃ℎ ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩)))}
67	9, 15, 26, 32, 41, 47, 58, 64, 65, 66	br8 33287	1 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ InnerFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1088   = wceq 1542   ∈ wcel 2113  ⟨cop 4519   class class class wbr 5027  ‘cfv 6333  ℕcn 11709  𝔼cee 26826   Btwn cbtwn 26827  Cgrccgr 26828   InnerFiveSeg cifs 33967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-v 3399  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-opab 5090  df-iota 6291  df-fv 6341  df-ifs 33972

This theorem is referenced by:  ifscgr  33976  cgrsub  33977  btwnxfr  33988  brifs2  34010  btwnconn1lem6  34024