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 35987
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 4878 . . . . 5 (𝑎 = 𝐴 → ⟨𝑎, 𝑐⟩ = ⟨𝐴, 𝑐⟩)
21breq2d 5160 . . . 4 (𝑎 = 𝐴 → (𝑏 Btwn ⟨𝑎, 𝑐⟩ ↔ 𝑏 Btwn ⟨𝐴, 𝑐⟩))
32anbi1d 631 . . 3 (𝑎 = 𝐴 → ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
4 opeq1 4878 . . . . 5 (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
54breq1d 5158 . . . 4 (𝑎 = 𝐴 → (⟨𝑎, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ↔ ⟨𝐴, 𝑏⟩Cgr⟨𝑒, 𝑓⟩))
65anbi1d 631 . . 3 (𝑎 = 𝐴 → ((⟨𝑎, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
7 opeq1 4878 . . . . 5 (𝑎 = 𝐴 → ⟨𝑎, 𝑑⟩ = ⟨𝐴, 𝑑⟩)
87breq1d 5158 . . . 4 (𝑎 = 𝐴 → (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩))
98anbi1d 631 . . 3 (𝑎 = 𝐴 → ((⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩)))
103, 6, 93anbi123d 1435 . 2 (𝑎 = 𝐴 → (((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩)) ↔ ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩))))
11 breq1 5151 . . . 4 (𝑏 = 𝐵 → (𝑏 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝑐⟩))
1211anbi1d 631 . . 3 (𝑏 = 𝐵 → ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
13 opeq2 4879 . . . . 5 (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
1413breq1d 5158 . . . 4 (𝑏 = 𝐵 → (⟨𝐴, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩))
15 opeq1 4878 . . . . 5 (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
1615breq1d 5158 . . . 4 (𝑏 = 𝐵 → (⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩))
1714, 16anbi12d 632 . . 3 (𝑏 = 𝐵 → ((⟨𝐴, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
18 opeq1 4878 . . . . 5 (𝑏 = 𝐵 → ⟨𝑏, 𝑑⟩ = ⟨𝐵, 𝑑⟩)
1918breq1d 5158 . . . 4 (𝑏 = 𝐵 → (⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩ ↔ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩))
2019anbi2d 630 . . 3 (𝑏 = 𝐵 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩)))
2112, 17, 203anbi123d 1435 . 2 (𝑏 = 𝐵 → (((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩))))
22 opeq2 4879 . . . . 5 (𝑐 = 𝐶 → ⟨𝐴, 𝑐⟩ = ⟨𝐴, 𝐶⟩)
2322breq2d 5160 . . . 4 (𝑐 = 𝐶 → (𝐵 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝐶⟩))
2423anbi1d 631 . . 3 (𝑐 = 𝐶 → ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
25 opeq2 4879 . . . . 5 (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
2625breq1d 5158 . . . 4 (𝑐 = 𝐶 → (⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩))
2726anbi2d 630 . . 3 (𝑐 = 𝐶 → ((⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
2824, 273anbi12d 1436 . 2 (𝑐 = 𝐶 → (((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩))))
29 opeq2 4879 . . . . 5 (𝑑 = 𝐷 → ⟨𝐴, 𝑑⟩ = ⟨𝐴, 𝐷⟩)
3029breq1d 5158 . . . 4 (𝑑 = 𝐷 → (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩))
31 opeq2 4879 . . . . 5 (𝑑 = 𝐷 → ⟨𝐵, 𝑑⟩ = ⟨𝐵, 𝐷⟩)
3231breq1d 5158 . . . 4 (𝑑 = 𝐷 → (⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩ ↔ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩))
3330, 32anbi12d 632 . . 3 (𝑑 = 𝐷 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩)))
34333anbi3d 1441 . 2 (𝑑 = 𝐷 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩))))
35 opeq1 4878 . . . . 5 (𝑒 = 𝐸 → ⟨𝑒, 𝑔⟩ = ⟨𝐸, 𝑔⟩)
3635breq2d 5160 . . . 4 (𝑒 = 𝐸 → (𝑓 Btwn ⟨𝑒, 𝑔⟩ ↔ 𝑓 Btwn ⟨𝐸, 𝑔⟩))
3736anbi2d 630 . . 3 (𝑒 = 𝐸 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩)))
38 opeq1 4878 . . . . 5 (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩)
3938breq2d 5160 . . . 4 (𝑒 = 𝐸 → (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝑓⟩))
4039anbi1d 631 . . 3 (𝑒 = 𝐸 → ((⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
41 opeq1 4878 . . . . 5 (𝑒 = 𝐸 → ⟨𝑒, ⟩ = ⟨𝐸, ⟩)
4241breq2d 5160 . . . 4 (𝑒 = 𝐸 → (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩))
4342anbi1d 631 . . 3 (𝑒 = 𝐸 → ((⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩)))
4437, 40, 433anbi123d 1435 . 2 (𝑒 = 𝐸 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩))))
45 breq1 5151 . . . 4 (𝑓 = 𝐹 → (𝑓 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝑔⟩))
4645anbi2d 630 . . 3 (𝑓 = 𝐹 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩)))
47 opeq2 4879 . . . . 5 (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩)
4847breq2d 5160 . . . 4 (𝑓 = 𝐹 → (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝑓⟩ ↔ ⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩))
49 opeq1 4878 . . . . 5 (𝑓 = 𝐹 → ⟨𝑓, 𝑔⟩ = ⟨𝐹, 𝑔⟩)
5049breq2d 5160 . . . 4 (𝑓 = 𝐹 → (⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩))
5148, 50anbi12d 632 . . 3 (𝑓 = 𝐹 → ((⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩)))
52 opeq1 4878 . . . . 5 (𝑓 = 𝐹 → ⟨𝑓, ⟩ = ⟨𝐹, ⟩)
5352breq2d 5160 . . . 4 (𝑓 = 𝐹 → (⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩ ↔ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩))
5453anbi2d 630 . . 3 (𝑓 = 𝐹 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩)))
5546, 51, 543anbi123d 1435 . 2 (𝑓 = 𝐹 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝑓⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩))))
56 opeq2 4879 . . . . 5 (𝑔 = 𝐺 → ⟨𝐸, 𝑔⟩ = ⟨𝐸, 𝐺⟩)
5756breq2d 5160 . . . 4 (𝑔 = 𝐺 → (𝐹 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝐺⟩))
5857anbi2d 630 . . 3 (𝑔 = 𝐺 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩)))
59 opeq2 4879 . . . . 5 (𝑔 = 𝐺 → ⟨𝐹, 𝑔⟩ = ⟨𝐹, 𝐺⟩)
6059breq2d 5160 . . . 4 (𝑔 = 𝐺 → (⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩))
6160anbi2d 630 . . 3 (𝑔 = 𝐺 → ((⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ↔ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)))
6258, 613anbi12d 1436 . 2 (𝑔 = 𝐺 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩))))
63 opeq2 4879 . . . . 5 ( = 𝐻 → ⟨𝐸, ⟩ = ⟨𝐸, 𝐻⟩)
6463breq2d 5160 . . . 4 ( = 𝐻 → (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩))
65 opeq2 4879 . . . . 5 ( = 𝐻 → ⟨𝐹, ⟩ = ⟨𝐹, 𝐻⟩)
6665breq2d 5160 . . . 4 ( = 𝐻 → (⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩ ↔ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
6764, 66anbi12d 632 . . 3 ( = 𝐻 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
68673anbi3d 1441 . 2 ( = 𝐻 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))))
69 fveq2 6907 . 2 (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁))
70 df-ofs 35965 . 2 OuterFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)∃𝑔 ∈ (𝔼‘𝑛)∃ ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑒, 𝑓⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ⟩)))}
7110, 21, 28, 34, 44, 55, 62, 68, 69, 70br8 35736 1 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ OuterFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐵⟩Cgr⟨𝐸, 𝐹⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  cop 4637   class class class wbr 5148  cfv 6563  cn 12264  𝔼cee 28918   Btwn cbtwn 28919  Cgrccgr 28920   OuterFiveSeg cofs 35964
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-iota 6516  df-fv 6571  df-ofs 35965
This theorem is referenced by:  5segofs  35988  ofscom  35989  cgrextend  35990  segconeq  35992  ifscgr  36026  brofs2  36059
  Copyright terms: Public domain W3C validator