Theorem brifs 35511

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 4866	. . . . 5 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑐⟩ = ⟨𝐴, 𝑐⟩)
2	1	breq2d 5151	. . . 4 ⊢ (𝑎 = 𝐴 → (𝑏 Btwn ⟨𝑎, 𝑐⟩ ↔ 𝑏 Btwn ⟨𝐴, 𝑐⟩))
3	2	anbi1d 629	. . 3 ⊢ (𝑎 = 𝐴 → ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
4	1	breq1d 5149	. . . 4 ⊢ (𝑎 = 𝐴 → (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩))
5	4	anbi1d 629	. . 3 ⊢ (𝑎 = 𝐴 → ((⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
6		opeq1 4866	. . . . 5 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑑⟩ = ⟨𝐴, 𝑑⟩)
7	6	breq1d 5149	. . . 4 ⊢ (𝑎 = 𝐴 → (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ↔ ⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩))
8	7	anbi1d 629	. . 3 ⊢ (𝑎 = 𝐴 → ((⟨𝑎, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩)))
9	3, 5, 8	3anbi123d 1432	. 2 ⊢ (𝑎 = 𝐴 → (((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩))))
10		breq1 5142	. . . 4 ⊢ (𝑏 = 𝐵 → (𝑏 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝑐⟩))
11	10	anbi1d 629	. . 3 ⊢ (𝑏 = 𝐵 → ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
12		opeq1 4866	. . . . 5 ⊢ (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
13	12	breq1d 5149	. . . 4 ⊢ (𝑏 = 𝐵 → (⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩))
14	13	anbi2d 628	. . 3 ⊢ (𝑏 = 𝐵 → ((⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
15	11, 14	3anbi12d 1433	. 2 ⊢ (𝑏 = 𝐵 → (((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩))))
16		opeq2 4867	. . . . 5 ⊢ (𝑐 = 𝐶 → ⟨𝐴, 𝑐⟩ = ⟨𝐴, 𝐶⟩)
17	16	breq2d 5151	. . . 4 ⊢ (𝑐 = 𝐶 → (𝐵 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝐶⟩))
18	17	anbi1d 629	. . 3 ⊢ (𝑐 = 𝐶 → ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
19	16	breq1d 5149	. . . 4 ⊢ (𝑐 = 𝐶 → (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩))
20		opeq2 4867	. . . . 5 ⊢ (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
21	20	breq1d 5149	. . . 4 ⊢ (𝑐 = 𝐶 → (⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩))
22	19, 21	anbi12d 630	. . 3 ⊢ (𝑐 = 𝐶 → ((⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
23		opeq1 4866	. . . . 5 ⊢ (𝑐 = 𝐶 → ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝑑⟩)
24	23	breq1d 5149	. . . 4 ⊢ (𝑐 = 𝐶 → (⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩ ↔ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ℎ⟩))
25	24	anbi2d 628	. . 3 ⊢ (𝑐 = 𝐶 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ℎ⟩)))
26	18, 22, 25	3anbi123d 1432	. 2 ⊢ (𝑐 = 𝐶 → (((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ℎ⟩))))
27		opeq2 4867	. . . . 5 ⊢ (𝑑 = 𝐷 → ⟨𝐴, 𝑑⟩ = ⟨𝐴, 𝐷⟩)
28	27	breq1d 5149	. . . 4 ⊢ (𝑑 = 𝐷 → (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩))
29		opeq2 4867	. . . . 5 ⊢ (𝑑 = 𝐷 → ⟨𝐶, 𝑑⟩ = ⟨𝐶, 𝐷⟩)
30	29	breq1d 5149	. . . 4 ⊢ (𝑑 = 𝐷 → (⟨𝐶, 𝑑⟩Cgr⟨𝑔, ℎ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩))
31	28, 30	anbi12d 630	. . 3 ⊢ (𝑑 = 𝐷 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ℎ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩)))
32	31	3anbi3d 1438	. 2 ⊢ (𝑑 = 𝐷 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩))))
33		opeq1 4866	. . . . 5 ⊢ (𝑒 = 𝐸 → ⟨𝑒, 𝑔⟩ = ⟨𝐸, 𝑔⟩)
34	33	breq2d 5151	. . . 4 ⊢ (𝑒 = 𝐸 → (𝑓 Btwn ⟨𝑒, 𝑔⟩ ↔ 𝑓 Btwn ⟨𝐸, 𝑔⟩))
35	34	anbi2d 628	. . 3 ⊢ (𝑒 = 𝐸 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩)))
36	33	breq2d 5151	. . . 4 ⊢ (𝑒 = 𝐸 → (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩))
37	36	anbi1d 629	. . 3 ⊢ (𝑒 = 𝐸 → ((⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
38		opeq1 4866	. . . . 5 ⊢ (𝑒 = 𝐸 → ⟨𝑒, ℎ⟩ = ⟨𝐸, ℎ⟩)
39	38	breq2d 5151	. . . 4 ⊢ (𝑒 = 𝐸 → (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩))
40	39	anbi1d 629	. . 3 ⊢ (𝑒 = 𝐸 → ((⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩)))
41	35, 37, 40	3anbi123d 1432	. 2 ⊢ (𝑒 = 𝐸 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩))))
42		breq1 5142	. . . 4 ⊢ (𝑓 = 𝐹 → (𝑓 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝑔⟩))
43	42	anbi2d 628	. . 3 ⊢ (𝑓 = 𝐹 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩)))
44		opeq1 4866	. . . . 5 ⊢ (𝑓 = 𝐹 → ⟨𝑓, 𝑔⟩ = ⟨𝐹, 𝑔⟩)
45	44	breq2d 5151	. . . 4 ⊢ (𝑓 = 𝐹 → (⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩))
46	45	anbi2d 628	. . 3 ⊢ (𝑓 = 𝐹 → ((⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩)))
47	43, 46	3anbi12d 1433	. 2 ⊢ (𝑓 = 𝐹 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩))))
48		opeq2 4867	. . . . 5 ⊢ (𝑔 = 𝐺 → ⟨𝐸, 𝑔⟩ = ⟨𝐸, 𝐺⟩)
49	48	breq2d 5151	. . . 4 ⊢ (𝑔 = 𝐺 → (𝐹 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝐺⟩))
50	49	anbi2d 628	. . 3 ⊢ (𝑔 = 𝐺 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩)))
51	48	breq2d 5151	. . . 4 ⊢ (𝑔 = 𝐺 → (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩))
52		opeq2 4867	. . . . 5 ⊢ (𝑔 = 𝐺 → ⟨𝐹, 𝑔⟩ = ⟨𝐹, 𝐺⟩)
53	52	breq2d 5151	. . . 4 ⊢ (𝑔 = 𝐺 → (⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩))
54	51, 53	anbi12d 630	. . 3 ⊢ (𝑔 = 𝐺 → ((⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)))
55		opeq1 4866	. . . . 5 ⊢ (𝑔 = 𝐺 → ⟨𝑔, ℎ⟩ = ⟨𝐺, ℎ⟩)
56	55	breq2d 5151	. . . 4 ⊢ (𝑔 = 𝐺 → (⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ℎ⟩))
57	56	anbi2d 628	. . 3 ⊢ (𝑔 = 𝐺 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ℎ⟩)))
58	50, 54, 57	3anbi123d 1432	. 2 ⊢ (𝑔 = 𝐺 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ℎ⟩))))
59		opeq2 4867	. . . . 5 ⊢ (ℎ = 𝐻 → ⟨𝐸, ℎ⟩ = ⟨𝐸, 𝐻⟩)
60	59	breq2d 5151	. . . 4 ⊢ (ℎ = 𝐻 → (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩))
61		opeq2 4867	. . . . 5 ⊢ (ℎ = 𝐻 → ⟨𝐺, ℎ⟩ = ⟨𝐺, 𝐻⟩)
62	61	breq2d 5151	. . . 4 ⊢ (ℎ = 𝐻 → (⟨𝐶, 𝐷⟩Cgr⟨𝐺, ℎ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
63	60, 62	anbi12d 630	. . 3 ⊢ (ℎ = 𝐻 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ℎ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
64	63	3anbi3d 1438	. 2 ⊢ (ℎ = 𝐻 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ℎ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
65		fveq2 6882	. 2 ⊢ (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁))
66		df-ifs 35508	. 2 ⊢ InnerFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)∃𝑔 ∈ (𝔼‘𝑛)∃ℎ ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ℎ⟩)))}
67	9, 15, 26, 32, 41, 47, 58, 64, 65, 66	br8 35222	1 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ InnerFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  ⟨cop 4627   class class class wbr 5139  ‘cfv 6534  ℕcn 12210  𝔼cee 28618   Btwn cbtwn 28619  Cgrccgr 28620   InnerFiveSeg cifs 35503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pr 5418

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-br 5140  df-opab 5202  df-iota 6486  df-fv 6542  df-ifs 35508

This theorem is referenced by:  ifscgr  35512  cgrsub  35513  btwnxfr  35524  brifs2  35546  btwnconn1lem6  35560