Theorem brofs 34044

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

Assertion

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

Proof of Theorem brofs

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

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2110  ⟨cop 4547   class class class wbr 5053  ‘cfv 6380  ℕcn 11830  𝔼cee 26979   Btwn cbtwn 26980  Cgrccgr 26981   OuterFiveSeg cofs 34021

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-iota 6338  df-fv 6388  df-ofs 34022

This theorem is referenced by:  5segofs  34045  ofscom  34046  cgrextend  34047  segconeq  34049  ifscgr  34083  brofs2  34116