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

Theorem brifs 33388
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.
StepHypRef Expression
1 opeq1 4802 . . . . 5 (𝑎 = 𝐴 → ⟨𝑎, 𝑐⟩ = ⟨𝐴, 𝑐⟩)
21breq2d 5075 . . . 4 (𝑎 = 𝐴 → (𝑏 Btwn ⟨𝑎, 𝑐⟩ ↔ 𝑏 Btwn ⟨𝐴, 𝑐⟩))
32anbi1d 629 . . 3 (𝑎 = 𝐴 → ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
41breq1d 5073 . . . 4 (𝑎 = 𝐴 → (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩))
54anbi1d 629 . . 3 (𝑎 = 𝐴 → ((⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
6 opeq1 4802 . . . . 5 (𝑎 = 𝐴 → ⟨𝑎, 𝑑⟩ = ⟨𝐴, 𝑑⟩)
76breq1d 5073 . . . 4 (𝑎 = 𝐴 → (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩))
87anbi1d 629 . . 3 (𝑎 = 𝐴 → ((⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)))
93, 5, 83anbi123d 1429 . 2 (𝑎 = 𝐴 → (((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)) ↔ ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩))))
10 breq1 5066 . . . 4 (𝑏 = 𝐵 → (𝑏 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝑐⟩))
1110anbi1d 629 . . 3 (𝑏 = 𝐵 → ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
12 opeq1 4802 . . . . 5 (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
1312breq1d 5073 . . . 4 (𝑏 = 𝐵 → (⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩))
1413anbi2d 628 . . 3 (𝑏 = 𝐵 → ((⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
1511, 143anbi12d 1430 . 2 (𝑏 = 𝐵 → (((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩))))
16 opeq2 4803 . . . . 5 (𝑐 = 𝐶 → ⟨𝐴, 𝑐⟩ = ⟨𝐴, 𝐶⟩)
1716breq2d 5075 . . . 4 (𝑐 = 𝐶 → (𝐵 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝐶⟩))
1817anbi1d 629 . . 3 (𝑐 = 𝐶 → ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
1916breq1d 5073 . . . 4 (𝑐 = 𝐶 → (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩))
20 opeq2 4803 . . . . 5 (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
2120breq1d 5073 . . . 4 (𝑐 = 𝐶 → (⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩))
2219, 21anbi12d 630 . . 3 (𝑐 = 𝐶 → ((⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
23 opeq1 4802 . . . . 5 (𝑐 = 𝐶 → ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝑑⟩)
2423breq1d 5073 . . . 4 (𝑐 = 𝐶 → (⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩ ↔ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩))
2524anbi2d 628 . . 3 (𝑐 = 𝐶 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩)))
2618, 22, 253anbi123d 1429 . 2 (𝑐 = 𝐶 → (((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩))))
27 opeq2 4803 . . . . 5 (𝑑 = 𝐷 → ⟨𝐴, 𝑑⟩ = ⟨𝐴, 𝐷⟩)
2827breq1d 5073 . . . 4 (𝑑 = 𝐷 → (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩))
29 opeq2 4803 . . . . 5 (𝑑 = 𝐷 → ⟨𝐶, 𝑑⟩ = ⟨𝐶, 𝐷⟩)
3029breq1d 5073 . . . 4 (𝑑 = 𝐷 → (⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩))
3128, 30anbi12d 630 . . 3 (𝑑 = 𝐷 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)))
32313anbi3d 1435 . 2 (𝑑 = 𝐷 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩))))
33 opeq1 4802 . . . . 5 (𝑒 = 𝐸 → ⟨𝑒, 𝑔⟩ = ⟨𝐸, 𝑔⟩)
3433breq2d 5075 . . . 4 (𝑒 = 𝐸 → (𝑓 Btwn ⟨𝑒, 𝑔⟩ ↔ 𝑓 Btwn ⟨𝐸, 𝑔⟩))
3534anbi2d 628 . . 3 (𝑒 = 𝐸 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩)))
3633breq2d 5075 . . . 4 (𝑒 = 𝐸 → (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩))
3736anbi1d 629 . . 3 (𝑒 = 𝐸 → ((⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
38 opeq1 4802 . . . . 5 (𝑒 = 𝐸 → ⟨𝑒, ⟩ = ⟨𝐸, ⟩)
3938breq2d 5075 . . . 4 (𝑒 = 𝐸 → (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩))
4039anbi1d 629 . . 3 (𝑒 = 𝐸 → ((⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)))
4135, 37, 403anbi123d 1429 . 2 (𝑒 = 𝐸 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩))))
42 breq1 5066 . . . 4 (𝑓 = 𝐹 → (𝑓 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝑔⟩))
4342anbi2d 628 . . 3 (𝑓 = 𝐹 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩)))
44 opeq1 4802 . . . . 5 (𝑓 = 𝐹 → ⟨𝑓, 𝑔⟩ = ⟨𝐹, 𝑔⟩)
4544breq2d 5075 . . . 4 (𝑓 = 𝐹 → (⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩))
4645anbi2d 628 . . 3 (𝑓 = 𝐹 → ((⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩)))
4743, 463anbi12d 1430 . 2 (𝑓 = 𝐹 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩))))
48 opeq2 4803 . . . . 5 (𝑔 = 𝐺 → ⟨𝐸, 𝑔⟩ = ⟨𝐸, 𝐺⟩)
4948breq2d 5075 . . . 4 (𝑔 = 𝐺 → (𝐹 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝐺⟩))
5049anbi2d 628 . . 3 (𝑔 = 𝐺 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩)))
5148breq2d 5075 . . . 4 (𝑔 = 𝐺 → (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩))
52 opeq2 4803 . . . . 5 (𝑔 = 𝐺 → ⟨𝐹, 𝑔⟩ = ⟨𝐹, 𝐺⟩)
5352breq2d 5075 . . . 4 (𝑔 = 𝐺 → (⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩))
5451, 53anbi12d 630 . . 3 (𝑔 = 𝐺 → ((⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)))
55 opeq1 4802 . . . . 5 (𝑔 = 𝐺 → ⟨𝑔, ⟩ = ⟨𝐺, ⟩)
5655breq2d 5075 . . . 4 (𝑔 = 𝐺 → (⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩))
5756anbi2d 628 . . 3 (𝑔 = 𝐺 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩)))
5850, 54, 573anbi123d 1429 . 2 (𝑔 = 𝐺 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩))))
59 opeq2 4803 . . . . 5 ( = 𝐻 → ⟨𝐸, ⟩ = ⟨𝐸, 𝐻⟩)
6059breq2d 5075 . . . 4 ( = 𝐻 → (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩))
61 opeq2 4803 . . . . 5 ( = 𝐻 → ⟨𝐺, ⟩ = ⟨𝐺, 𝐻⟩)
6261breq2d 5075 . . . 4 ( = 𝐻 → (⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
6360, 62anbi12d 630 . . 3 ( = 𝐻 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
64633anbi3d 1435 . 2 ( = 𝐻 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
65 fveq2 6667 . 2 (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁))
66 df-ifs 33385 . 2 InnerFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)∃𝑔 ∈ (𝔼‘𝑛)∃ ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)))}
679, 15, 26, 32, 41, 47, 58, 64, 65, 66br8 32876 1 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ InnerFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107  cop 4570   class class class wbr 5063  cfv 6352  cn 11627  𝔼cee 26588   Btwn cbtwn 26589  Cgrccgr 26590   InnerFiveSeg cifs 33380
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-iota 6312  df-fv 6360  df-ifs 33385
This theorem is referenced by:  ifscgr  33389  cgrsub  33390  btwnxfr  33401  brifs2  33423  btwnconn1lem6  33437
  Copyright terms: Public domain W3C validator