Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brofs Structured version   Visualization version   GIF version

Theorem brofs 35499
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.
StepHypRef Expression
1 opeq1 4866 . . . . 5 (𝑎 = 𝐴 → ⟨𝑎, 𝑐⟩ = ⟨𝐴, 𝑐⟩)
21breq2d 5151 . . . 4 (𝑎 = 𝐴 → (𝑏 Btwn ⟨𝑎, 𝑐⟩ ↔ 𝑏 Btwn ⟨𝐴, 𝑐⟩))
32anbi1d 629 . . 3 (𝑎 = 𝐴 → ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
4 opeq1 4866 . . . . 5 (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
54breq1d 5149 . . . 4 (𝑎 = 𝐴 → (⟨𝑎, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ↔ ⟨𝐴, 𝑏⟩Cgr⟨𝑒, 𝑓⟩))
65anbi1d 629 . . 3 (𝑎 = 𝐴 → ((⟨𝑎, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
7 opeq1 4866 . . . . 5 (𝑎 = 𝐴 → ⟨𝑎, 𝑑⟩ = ⟨𝐴, 𝑑⟩)
87breq1d 5149 . . . 4 (𝑎 = 𝐴 → (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩))
98anbi1d 629 . . 3 (𝑎 = 𝐴 → ((⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩)))
103, 6, 93anbi123d 1432 . 2 (𝑎 = 𝐴 → (((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩)) ↔ ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩))))
11 breq1 5142 . . . 4 (𝑏 = 𝐵 → (𝑏 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝑐⟩))
1211anbi1d 629 . . 3 (𝑏 = 𝐵 → ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
13 opeq2 4867 . . . . 5 (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
1413breq1d 5149 . . . 4 (𝑏 = 𝐵 → (⟨𝐴, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩))
15 opeq1 4866 . . . . 5 (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
1615breq1d 5149 . . . 4 (𝑏 = 𝐵 → (⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩))
1714, 16anbi12d 630 . . 3 (𝑏 = 𝐵 → ((⟨𝐴, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
18 opeq1 4866 . . . . 5 (𝑏 = 𝐵 → ⟨𝑏, 𝑑⟩ = ⟨𝐵, 𝑑⟩)
1918breq1d 5149 . . . 4 (𝑏 = 𝐵 → (⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩ ↔ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩))
2019anbi2d 628 . . 3 (𝑏 = 𝐵 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩)))
2112, 17, 203anbi123d 1432 . 2 (𝑏 = 𝐵 → (((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩))))
22 opeq2 4867 . . . . 5 (𝑐 = 𝐶 → ⟨𝐴, 𝑐⟩ = ⟨𝐴, 𝐶⟩)
2322breq2d 5151 . . . 4 (𝑐 = 𝐶 → (𝐵 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝐶⟩))
2423anbi1d 629 . . 3 (𝑐 = 𝐶 → ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
25 opeq2 4867 . . . . 5 (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
2625breq1d 5149 . . . 4 (𝑐 = 𝐶 → (⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩))
2726anbi2d 628 . . 3 (𝑐 = 𝐶 → ((⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
2824, 273anbi12d 1433 . 2 (𝑐 = 𝐶 → (((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩))))
29 opeq2 4867 . . . . 5 (𝑑 = 𝐷 → ⟨𝐴, 𝑑⟩ = ⟨𝐴, 𝐷⟩)
3029breq1d 5149 . . . 4 (𝑑 = 𝐷 → (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩))
31 opeq2 4867 . . . . 5 (𝑑 = 𝐷 → ⟨𝐵, 𝑑⟩ = ⟨𝐵, 𝐷⟩)
3231breq1d 5149 . . . 4 (𝑑 = 𝐷 → (⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩ ↔ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩))
3330, 32anbi12d 630 . . 3 (𝑑 = 𝐷 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩)))
34333anbi3d 1438 . 2 (𝑑 = 𝐷 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩))))
35 opeq1 4866 . . . . 5 (𝑒 = 𝐸 → ⟨𝑒, 𝑔⟩ = ⟨𝐸, 𝑔⟩)
3635breq2d 5151 . . . 4 (𝑒 = 𝐸 → (𝑓 Btwn ⟨𝑒, 𝑔⟩ ↔ 𝑓 Btwn ⟨𝐸, 𝑔⟩))
3736anbi2d 628 . . 3 (𝑒 = 𝐸 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩)))
38 opeq1 4866 . . . . 5 (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩)
3938breq2d 5151 . . . 4 (𝑒 = 𝐸 → (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝑓⟩))
4039anbi1d 629 . . 3 (𝑒 = 𝐸 → ((⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
41 opeq1 4866 . . . . 5 (𝑒 = 𝐸 → ⟨𝑒, ⟩ = ⟨𝐸, ⟩)
4241breq2d 5151 . . . 4 (𝑒 = 𝐸 → (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩))
4342anbi1d 629 . . 3 (𝑒 = 𝐸 → ((⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩)))
4437, 40, 433anbi123d 1432 . 2 (𝑒 = 𝐸 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩))))
45 breq1 5142 . . . 4 (𝑓 = 𝐹 → (𝑓 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝑔⟩))
4645anbi2d 628 . . 3 (𝑓 = 𝐹 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩)))
47 opeq2 4867 . . . . 5 (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩)
4847breq2d 5151 . . . 4 (𝑓 = 𝐹 → (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝑓⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩))
49 opeq1 4866 . . . . 5 (𝑓 = 𝐹 → ⟨𝑓, 𝑔⟩ = ⟨𝐹, 𝑔⟩)
5049breq2d 5151 . . . 4 (𝑓 = 𝐹 → (⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩))
5148, 50anbi12d 630 . . 3 (𝑓 = 𝐹 → ((⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩)))
52 opeq1 4866 . . . . 5 (𝑓 = 𝐹 → ⟨𝑓, ⟩ = ⟨𝐹, ⟩)
5352breq2d 5151 . . . 4 (𝑓 = 𝐹 → (⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩ ↔ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩))
5453anbi2d 628 . . 3 (𝑓 = 𝐹 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩)))
5546, 51, 543anbi123d 1432 . 2 (𝑓 = 𝐹 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩))))
56 opeq2 4867 . . . . 5 (𝑔 = 𝐺 → ⟨𝐸, 𝑔⟩ = ⟨𝐸, 𝐺⟩)
5756breq2d 5151 . . . 4 (𝑔 = 𝐺 → (𝐹 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝐺⟩))
5857anbi2d 628 . . 3 (𝑔 = 𝐺 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩)))
59 opeq2 4867 . . . . 5 (𝑔 = 𝐺 → ⟨𝐹, 𝑔⟩ = ⟨𝐹, 𝐺⟩)
6059breq2d 5151 . . . 4 (𝑔 = 𝐺 → (⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩))
6160anbi2d 628 . . 3 (𝑔 = 𝐺 → ((⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)))
6258, 613anbi12d 1433 . 2 (𝑔 = 𝐺 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩))))
63 opeq2 4867 . . . . 5 ( = 𝐻 → ⟨𝐸, ⟩ = ⟨𝐸, 𝐻⟩)
6463breq2d 5151 . . . 4 ( = 𝐻 → (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩))
65 opeq2 4867 . . . . 5 ( = 𝐻 → ⟨𝐹, ⟩ = ⟨𝐹, 𝐻⟩)
6665breq2d 5151 . . . 4 ( = 𝐻 → (⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩ ↔ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
6764, 66anbi12d 630 . . 3 ( = 𝐻 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
68673anbi3d 1438 . 2 ( = 𝐻 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))))
69 fveq2 6882 . 2 (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁))
70 df-ofs 35477 . 2 OuterFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)∃𝑔 ∈ (𝔼‘𝑛)∃ ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩)))}
7110, 21, 28, 34, 44, 55, 62, 68, 69, 70br8 35248 1 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  cop 4627   class class class wbr 5139  cfv 6534  cn 12211  𝔼cee 28639   Btwn cbtwn 28640  Cgrccgr 28641   OuterFiveSeg cofs 35476
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-ofs 35477
This theorem is referenced by:  5segofs  35500  ofscom  35501  cgrextend  35502  segconeq  35504  ifscgr  35538  brofs2  35571
  Copyright terms: Public domain W3C validator