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 32469
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 4595 . . . . 5 (𝑎 = 𝐴 → ⟨𝑎, 𝑐⟩ = ⟨𝐴, 𝑐⟩)
21breq2d 4856 . . . 4 (𝑎 = 𝐴 → (𝑏 Btwn ⟨𝑎, 𝑐⟩ ↔ 𝑏 Btwn ⟨𝐴, 𝑐⟩))
32anbi1d 617 . . 3 (𝑎 = 𝐴 → ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
41breq1d 4854 . . . 4 (𝑎 = 𝐴 → (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩))
54anbi1d 617 . . 3 (𝑎 = 𝐴 → ((⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
6 opeq1 4595 . . . . 5 (𝑎 = 𝐴 → ⟨𝑎, 𝑑⟩ = ⟨𝐴, 𝑑⟩)
76breq1d 4854 . . . 4 (𝑎 = 𝐴 → (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩))
87anbi1d 617 . . 3 (𝑎 = 𝐴 → ((⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)))
93, 5, 83anbi123d 1553 . 2 (𝑎 = 𝐴 → (((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)) ↔ ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩))))
10 breq1 4847 . . . 4 (𝑏 = 𝐵 → (𝑏 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝑐⟩))
1110anbi1d 617 . . 3 (𝑏 = 𝐵 → ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
12 opeq1 4595 . . . . 5 (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
1312breq1d 4854 . . . 4 (𝑏 = 𝐵 → (⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩))
1413anbi2d 616 . . 3 (𝑏 = 𝐵 → ((⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
1511, 143anbi12d 1554 . 2 (𝑏 = 𝐵 → (((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩))))
16 opeq2 4596 . . . . 5 (𝑐 = 𝐶 → ⟨𝐴, 𝑐⟩ = ⟨𝐴, 𝐶⟩)
1716breq2d 4856 . . . 4 (𝑐 = 𝐶 → (𝐵 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝐶⟩))
1817anbi1d 617 . . 3 (𝑐 = 𝐶 → ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
1916breq1d 4854 . . . 4 (𝑐 = 𝐶 → (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩))
20 opeq2 4596 . . . . 5 (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
2120breq1d 4854 . . . 4 (𝑐 = 𝐶 → (⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩))
2219, 21anbi12d 618 . . 3 (𝑐 = 𝐶 → ((⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
23 opeq1 4595 . . . . 5 (𝑐 = 𝐶 → ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝑑⟩)
2423breq1d 4854 . . . 4 (𝑐 = 𝐶 → (⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩ ↔ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩))
2524anbi2d 616 . . 3 (𝑐 = 𝐶 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩)))
2618, 22, 253anbi123d 1553 . 2 (𝑐 = 𝐶 → (((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩))))
27 opeq2 4596 . . . . 5 (𝑑 = 𝐷 → ⟨𝐴, 𝑑⟩ = ⟨𝐴, 𝐷⟩)
2827breq1d 4854 . . . 4 (𝑑 = 𝐷 → (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩))
29 opeq2 4596 . . . . 5 (𝑑 = 𝐷 → ⟨𝐶, 𝑑⟩ = ⟨𝐶, 𝐷⟩)
3029breq1d 4854 . . . 4 (𝑑 = 𝐷 → (⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩))
3128, 30anbi12d 618 . . 3 (𝑑 = 𝐷 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)))
32313anbi3d 1559 . 2 (𝑑 = 𝐷 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩))))
33 opeq1 4595 . . . . 5 (𝑒 = 𝐸 → ⟨𝑒, 𝑔⟩ = ⟨𝐸, 𝑔⟩)
3433breq2d 4856 . . . 4 (𝑒 = 𝐸 → (𝑓 Btwn ⟨𝑒, 𝑔⟩ ↔ 𝑓 Btwn ⟨𝐸, 𝑔⟩))
3534anbi2d 616 . . 3 (𝑒 = 𝐸 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩)))
3633breq2d 4856 . . . 4 (𝑒 = 𝐸 → (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩))
3736anbi1d 617 . . 3 (𝑒 = 𝐸 → ((⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
38 opeq1 4595 . . . . 5 (𝑒 = 𝐸 → ⟨𝑒, ⟩ = ⟨𝐸, ⟩)
3938breq2d 4856 . . . 4 (𝑒 = 𝐸 → (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩))
4039anbi1d 617 . . 3 (𝑒 = 𝐸 → ((⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)))
4135, 37, 403anbi123d 1553 . 2 (𝑒 = 𝐸 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩))))
42 breq1 4847 . . . 4 (𝑓 = 𝐹 → (𝑓 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝑔⟩))
4342anbi2d 616 . . 3 (𝑓 = 𝐹 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩)))
44 opeq1 4595 . . . . 5 (𝑓 = 𝐹 → ⟨𝑓, 𝑔⟩ = ⟨𝐹, 𝑔⟩)
4544breq2d 4856 . . . 4 (𝑓 = 𝐹 → (⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩))
4645anbi2d 616 . . 3 (𝑓 = 𝐹 → ((⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩)))
4743, 463anbi12d 1554 . 2 (𝑓 = 𝐹 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩))))
48 opeq2 4596 . . . . 5 (𝑔 = 𝐺 → ⟨𝐸, 𝑔⟩ = ⟨𝐸, 𝐺⟩)
4948breq2d 4856 . . . 4 (𝑔 = 𝐺 → (𝐹 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝐺⟩))
5049anbi2d 616 . . 3 (𝑔 = 𝐺 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩)))
5148breq2d 4856 . . . 4 (𝑔 = 𝐺 → (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩))
52 opeq2 4596 . . . . 5 (𝑔 = 𝐺 → ⟨𝐹, 𝑔⟩ = ⟨𝐹, 𝐺⟩)
5352breq2d 4856 . . . 4 (𝑔 = 𝐺 → (⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩))
5451, 53anbi12d 618 . . 3 (𝑔 = 𝐺 → ((⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)))
55 opeq1 4595 . . . . 5 (𝑔 = 𝐺 → ⟨𝑔, ⟩ = ⟨𝐺, ⟩)
5655breq2d 4856 . . . 4 (𝑔 = 𝐺 → (⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩))
5756anbi2d 616 . . 3 (𝑔 = 𝐺 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩)))
5850, 54, 573anbi123d 1553 . 2 (𝑔 = 𝐺 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩))))
59 opeq2 4596 . . . . 5 ( = 𝐻 → ⟨𝐸, ⟩ = ⟨𝐸, 𝐻⟩)
6059breq2d 4856 . . . 4 ( = 𝐻 → (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩))
61 opeq2 4596 . . . . 5 ( = 𝐻 → ⟨𝐺, ⟩ = ⟨𝐺, 𝐻⟩)
6261breq2d 4856 . . . 4 ( = 𝐻 → (⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
6360, 62anbi12d 618 . . 3 ( = 𝐻 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
64633anbi3d 1559 . 2 ( = 𝐻 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
65 fveq2 6404 . 2 (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁))
66 df-ifs 32466 . 2 InnerFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)∃𝑔 ∈ (𝔼‘𝑛)∃ ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)))}
679, 15, 26, 32, 41, 47, 58, 64, 65, 66br8 31966 1 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ InnerFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  cop 4376   class class class wbr 4844  cfv 6097  cn 11301  𝔼cee 25981   Btwn cbtwn 25982  Cgrccgr 25983   InnerFiveSeg cifs 32461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-iota 6060  df-fv 6105  df-ifs 32466
This theorem is referenced by:  ifscgr  32470  cgrsub  32471  btwnxfr  32482  brifs2  32504  btwnconn1lem6  32518
  Copyright terms: Public domain W3C validator