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 32125
Description: Binary relationship 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 4393 . . . . 5 (𝑎 = 𝐴 → ⟨𝑎, 𝑐⟩ = ⟨𝐴, 𝑐⟩)
21breq2d 4656 . . . 4 (𝑎 = 𝐴 → (𝑏 Btwn ⟨𝑎, 𝑐⟩ ↔ 𝑏 Btwn ⟨𝐴, 𝑐⟩))
32anbi1d 740 . . 3 (𝑎 = 𝐴 → ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
41breq1d 4654 . . . 4 (𝑎 = 𝐴 → (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩))
54anbi1d 740 . . 3 (𝑎 = 𝐴 → ((⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
6 opeq1 4393 . . . . 5 (𝑎 = 𝐴 → ⟨𝑎, 𝑑⟩ = ⟨𝐴, 𝑑⟩)
76breq1d 4654 . . . 4 (𝑎 = 𝐴 → (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩))
87anbi1d 740 . . 3 (𝑎 = 𝐴 → ((⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)))
93, 5, 83anbi123d 1397 . 2 (𝑎 = 𝐴 → (((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)) ↔ ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩))))
10 breq1 4647 . . . 4 (𝑏 = 𝐵 → (𝑏 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝑐⟩))
1110anbi1d 740 . . 3 (𝑏 = 𝐵 → ((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
12 opeq1 4393 . . . . 5 (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
1312breq1d 4654 . . . 4 (𝑏 = 𝐵 → (⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩))
1413anbi2d 739 . . 3 (𝑏 = 𝐵 → ((⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩)))
1511, 143anbi12d 1398 . 2 (𝑏 = 𝐵 → (((𝑏 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩))))
16 opeq2 4394 . . . . 5 (𝑐 = 𝐶 → ⟨𝐴, 𝑐⟩ = ⟨𝐴, 𝐶⟩)
1716breq2d 4656 . . . 4 (𝑐 = 𝐶 → (𝐵 Btwn ⟨𝐴, 𝑐⟩ ↔ 𝐵 Btwn ⟨𝐴, 𝐶⟩))
1817anbi1d 740 . . 3 (𝑐 = 𝐶 → ((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩)))
1916breq1d 4654 . . . 4 (𝑐 = 𝐶 → (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩))
20 opeq2 4394 . . . . 5 (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
2120breq1d 4654 . . . 4 (𝑐 = 𝐶 → (⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩))
2219, 21anbi12d 746 . . 3 (𝑐 = 𝐶 → ((⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
23 opeq1 4393 . . . . 5 (𝑐 = 𝐶 → ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝑑⟩)
2423breq1d 4654 . . . 4 (𝑐 = 𝐶 → (⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩ ↔ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩))
2524anbi2d 739 . . 3 (𝑐 = 𝐶 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩)))
2618, 22, 253anbi123d 1397 . 2 (𝑐 = 𝐶 → (((𝐵 Btwn ⟨𝐴, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩))))
27 opeq2 4394 . . . . 5 (𝑑 = 𝐷 → ⟨𝐴, 𝑑⟩ = ⟨𝐴, 𝐷⟩)
2827breq1d 4654 . . . 4 (𝑑 = 𝐷 → (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩))
29 opeq2 4394 . . . . 5 (𝑑 = 𝐷 → ⟨𝐶, 𝑑⟩ = ⟨𝐶, 𝐷⟩)
3029breq1d 4654 . . . 4 (𝑑 = 𝐷 → (⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩))
3128, 30anbi12d 746 . . 3 (𝑑 = 𝐷 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)))
32313anbi3d 1403 . 2 (𝑑 = 𝐷 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝑑⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩))))
33 opeq1 4393 . . . . 5 (𝑒 = 𝐸 → ⟨𝑒, 𝑔⟩ = ⟨𝐸, 𝑔⟩)
3433breq2d 4656 . . . 4 (𝑒 = 𝐸 → (𝑓 Btwn ⟨𝑒, 𝑔⟩ ↔ 𝑓 Btwn ⟨𝐸, 𝑔⟩))
3534anbi2d 739 . . 3 (𝑒 = 𝐸 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩)))
3633breq2d 4656 . . . 4 (𝑒 = 𝐸 → (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩))
3736anbi1d 740 . . 3 (𝑒 = 𝐸 → ((⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩)))
38 opeq1 4393 . . . . 5 (𝑒 = 𝐸 → ⟨𝑒, ⟩ = ⟨𝐸, ⟩)
3938breq2d 4656 . . . 4 (𝑒 = 𝐸 → (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩))
4039anbi1d 740 . . 3 (𝑒 = 𝐸 → ((⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)))
4135, 37, 403anbi123d 1397 . 2 (𝑒 = 𝐸 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩))))
42 breq1 4647 . . . 4 (𝑓 = 𝐹 → (𝑓 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝑔⟩))
4342anbi2d 739 . . 3 (𝑓 = 𝐹 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩)))
44 opeq1 4393 . . . . 5 (𝑓 = 𝐹 → ⟨𝑓, 𝑔⟩ = ⟨𝐹, 𝑔⟩)
4544breq2d 4656 . . . 4 (𝑓 = 𝐹 → (⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩))
4645anbi2d 739 . . 3 (𝑓 = 𝐹 → ((⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩)))
4743, 463anbi12d 1398 . 2 (𝑓 = 𝐹 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝑓 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩))))
48 opeq2 4394 . . . . 5 (𝑔 = 𝐺 → ⟨𝐸, 𝑔⟩ = ⟨𝐸, 𝐺⟩)
4948breq2d 4656 . . . 4 (𝑔 = 𝐺 → (𝐹 Btwn ⟨𝐸, 𝑔⟩ ↔ 𝐹 Btwn ⟨𝐸, 𝐺⟩))
5049anbi2d 739 . . 3 (𝑔 = 𝐺 → ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ↔ (𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩)))
5148breq2d 4656 . . . 4 (𝑔 = 𝐺 → (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ↔ ⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩))
52 opeq2 4394 . . . . 5 (𝑔 = 𝐺 → ⟨𝐹, 𝑔⟩ = ⟨𝐹, 𝐺⟩)
5352breq2d 4656 . . . 4 (𝑔 = 𝐺 → (⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩ ↔ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩))
5451, 53anbi12d 746 . . 3 (𝑔 = 𝐺 → ((⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ↔ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩)))
55 opeq1 4393 . . . . 5 (𝑔 = 𝐺 → ⟨𝑔, ⟩ = ⟨𝐺, ⟩)
5655breq2d 4656 . . . 4 (𝑔 = 𝐺 → (⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩))
5756anbi2d 739 . . 3 (𝑔 = 𝐺 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩)))
5850, 54, 573anbi123d 1397 . 2 (𝑔 = 𝐺 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝑔⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝑔⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝑔⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝑔, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩))))
59 opeq2 4394 . . . . 5 ( = 𝐻 → ⟨𝐸, ⟩ = ⟨𝐸, 𝐻⟩)
6059breq2d 4656 . . . 4 ( = 𝐻 → (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩))
61 opeq2 4394 . . . . 5 ( = 𝐻 → ⟨𝐺, ⟩ = ⟨𝐺, 𝐻⟩)
6261breq2d 4656 . . . 4 ( = 𝐻 → (⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩ ↔ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))
6360, 62anbi12d 746 . . 3 ( = 𝐻 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩)))
64633anbi3d 1403 . 2 ( = 𝐻 → (((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, ⟩)) ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
65 fveq2 6178 . 2 (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁))
66 df-ifs 32122 . 2 InnerFiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)∃𝑔 ∈ (𝔼‘𝑛)∃ ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑓 Btwn ⟨𝑒, 𝑔⟩) ∧ (⟨𝑎, 𝑐⟩Cgr⟨𝑒, 𝑔⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑓, 𝑔⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ⟩ ∧ ⟨𝑐, 𝑑⟩Cgr⟨𝑔, ⟩)))}
679, 15, 26, 32, 41, 47, 58, 64, 65, 66br8 31621 1 (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ InnerFiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ((𝐵 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐹 Btwn ⟨𝐸, 𝐺⟩) ∧ (⟨𝐴, 𝐶⟩Cgr⟨𝐸, 𝐺⟩ ∧ ⟨𝐵, 𝐶⟩Cgr⟨𝐹, 𝐺⟩) ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐶, 𝐷⟩Cgr⟨𝐺, 𝐻⟩))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1481  wcel 1988  cop 4174   class class class wbr 4644  cfv 5876  cn 11005  𝔼cee 25749   Btwn cbtwn 25750  Cgrccgr 25751   InnerFiveSeg cifs 32117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-iota 5839  df-fv 5884  df-ifs 32122
This theorem is referenced by:  ifscgr  32126  cgrsub  32127  btwnxfr  32138  brifs2  32160  btwnconn1lem6  32174
  Copyright terms: Public domain W3C validator