| Step | Hyp | Ref
| Expression |
| 1 | | opeq1 4873 |
. . . . 5
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑐〉 = 〈𝐴, 𝑐〉) |
| 2 | 1 | breq2d 5155 |
. . . 4
⊢ (𝑎 = 𝐴 → (𝑏 Btwn 〈𝑎, 𝑐〉 ↔ 𝑏 Btwn 〈𝐴, 𝑐〉)) |
| 3 | 2 | anbi1d 631 |
. . 3
⊢ (𝑎 = 𝐴 → ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ↔ (𝑏 Btwn 〈𝐴, 𝑐〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉))) |
| 4 | | opeq1 4873 |
. . . . 5
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) |
| 5 | 4 | breq1d 5153 |
. . . 4
⊢ (𝑎 = 𝐴 → (〈𝑎, 𝑏〉Cgr〈𝑒, 𝑓〉 ↔ 〈𝐴, 𝑏〉Cgr〈𝑒, 𝑓〉)) |
| 6 | 5 | anbi1d 631 |
. . 3
⊢ (𝑎 = 𝐴 → ((〈𝑎, 𝑏〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑓, 𝑔〉) ↔ (〈𝐴, 𝑏〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑓, 𝑔〉))) |
| 7 | | opeq1 4873 |
. . . . 5
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑑〉 = 〈𝐴, 𝑑〉) |
| 8 | 7 | breq1d 5153 |
. . . 4
⊢ (𝑎 = 𝐴 → (〈𝑎, 𝑑〉Cgr〈𝑒, ℎ〉 ↔ 〈𝐴, 𝑑〉Cgr〈𝑒, ℎ〉)) |
| 9 | 8 | anbi1d 631 |
. . 3
⊢ (𝑎 = 𝐴 → ((〈𝑎, 𝑑〉Cgr〈𝑒, ℎ〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑓, ℎ〉) ↔ (〈𝐴, 𝑑〉Cgr〈𝑒, ℎ〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑓, ℎ〉))) |
| 10 | 3, 6, 9 | 3anbi123d 1438 |
. 2
⊢ (𝑎 = 𝐴 → (((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ∧ (〈𝑎, 𝑏〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑓, 𝑔〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑒, ℎ〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑓, ℎ〉)) ↔ ((𝑏 Btwn 〈𝐴, 𝑐〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ∧ (〈𝐴, 𝑏〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑓, 𝑔〉) ∧ (〈𝐴, 𝑑〉Cgr〈𝑒, ℎ〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑓, ℎ〉)))) |
| 11 | | breq1 5146 |
. . . 4
⊢ (𝑏 = 𝐵 → (𝑏 Btwn 〈𝐴, 𝑐〉 ↔ 𝐵 Btwn 〈𝐴, 𝑐〉)) |
| 12 | 11 | anbi1d 631 |
. . 3
⊢ (𝑏 = 𝐵 → ((𝑏 Btwn 〈𝐴, 𝑐〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ↔ (𝐵 Btwn 〈𝐴, 𝑐〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉))) |
| 13 | | opeq2 4874 |
. . . . 5
⊢ (𝑏 = 𝐵 → 〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉) |
| 14 | 13 | breq1d 5153 |
. . . 4
⊢ (𝑏 = 𝐵 → (〈𝐴, 𝑏〉Cgr〈𝑒, 𝑓〉 ↔ 〈𝐴, 𝐵〉Cgr〈𝑒, 𝑓〉)) |
| 15 | | opeq1 4873 |
. . . . 5
⊢ (𝑏 = 𝐵 → 〈𝑏, 𝑐〉 = 〈𝐵, 𝑐〉) |
| 16 | 15 | breq1d 5153 |
. . . 4
⊢ (𝑏 = 𝐵 → (〈𝑏, 𝑐〉Cgr〈𝑓, 𝑔〉 ↔ 〈𝐵, 𝑐〉Cgr〈𝑓, 𝑔〉)) |
| 17 | 14, 16 | anbi12d 632 |
. . 3
⊢ (𝑏 = 𝐵 → ((〈𝐴, 𝑏〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑓, 𝑔〉) ↔ (〈𝐴, 𝐵〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝐵, 𝑐〉Cgr〈𝑓, 𝑔〉))) |
| 18 | | opeq1 4873 |
. . . . 5
⊢ (𝑏 = 𝐵 → 〈𝑏, 𝑑〉 = 〈𝐵, 𝑑〉) |
| 19 | 18 | breq1d 5153 |
. . . 4
⊢ (𝑏 = 𝐵 → (〈𝑏, 𝑑〉Cgr〈𝑓, ℎ〉 ↔ 〈𝐵, 𝑑〉Cgr〈𝑓, ℎ〉)) |
| 20 | 19 | anbi2d 630 |
. . 3
⊢ (𝑏 = 𝐵 → ((〈𝐴, 𝑑〉Cgr〈𝑒, ℎ〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑓, ℎ〉) ↔ (〈𝐴, 𝑑〉Cgr〈𝑒, ℎ〉 ∧ 〈𝐵, 𝑑〉Cgr〈𝑓, ℎ〉))) |
| 21 | 12, 17, 20 | 3anbi123d 1438 |
. 2
⊢ (𝑏 = 𝐵 → (((𝑏 Btwn 〈𝐴, 𝑐〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ∧ (〈𝐴, 𝑏〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑓, 𝑔〉) ∧ (〈𝐴, 𝑑〉Cgr〈𝑒, ℎ〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑓, ℎ〉)) ↔ ((𝐵 Btwn 〈𝐴, 𝑐〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝐵, 𝑐〉Cgr〈𝑓, 𝑔〉) ∧ (〈𝐴, 𝑑〉Cgr〈𝑒, ℎ〉 ∧ 〈𝐵, 𝑑〉Cgr〈𝑓, ℎ〉)))) |
| 22 | | opeq2 4874 |
. . . . 5
⊢ (𝑐 = 𝐶 → 〈𝐴, 𝑐〉 = 〈𝐴, 𝐶〉) |
| 23 | 22 | breq2d 5155 |
. . . 4
⊢ (𝑐 = 𝐶 → (𝐵 Btwn 〈𝐴, 𝑐〉 ↔ 𝐵 Btwn 〈𝐴, 𝐶〉)) |
| 24 | 23 | anbi1d 631 |
. . 3
⊢ (𝑐 = 𝐶 → ((𝐵 Btwn 〈𝐴, 𝑐〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ↔ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉))) |
| 25 | | opeq2 4874 |
. . . . 5
⊢ (𝑐 = 𝐶 → 〈𝐵, 𝑐〉 = 〈𝐵, 𝐶〉) |
| 26 | 25 | breq1d 5153 |
. . . 4
⊢ (𝑐 = 𝐶 → (〈𝐵, 𝑐〉Cgr〈𝑓, 𝑔〉 ↔ 〈𝐵, 𝐶〉Cgr〈𝑓, 𝑔〉)) |
| 27 | 26 | anbi2d 630 |
. . 3
⊢ (𝑐 = 𝐶 → ((〈𝐴, 𝐵〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝐵, 𝑐〉Cgr〈𝑓, 𝑔〉) ↔ (〈𝐴, 𝐵〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝑓, 𝑔〉))) |
| 28 | 24, 27 | 3anbi12d 1439 |
. 2
⊢ (𝑐 = 𝐶 → (((𝐵 Btwn 〈𝐴, 𝑐〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝐵, 𝑐〉Cgr〈𝑓, 𝑔〉) ∧ (〈𝐴, 𝑑〉Cgr〈𝑒, ℎ〉 ∧ 〈𝐵, 𝑑〉Cgr〈𝑓, ℎ〉)) ↔ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝑓, 𝑔〉) ∧ (〈𝐴, 𝑑〉Cgr〈𝑒, ℎ〉 ∧ 〈𝐵, 𝑑〉Cgr〈𝑓, ℎ〉)))) |
| 29 | | opeq2 4874 |
. . . . 5
⊢ (𝑑 = 𝐷 → 〈𝐴, 𝑑〉 = 〈𝐴, 𝐷〉) |
| 30 | 29 | breq1d 5153 |
. . . 4
⊢ (𝑑 = 𝐷 → (〈𝐴, 𝑑〉Cgr〈𝑒, ℎ〉 ↔ 〈𝐴, 𝐷〉Cgr〈𝑒, ℎ〉)) |
| 31 | | opeq2 4874 |
. . . . 5
⊢ (𝑑 = 𝐷 → 〈𝐵, 𝑑〉 = 〈𝐵, 𝐷〉) |
| 32 | 31 | breq1d 5153 |
. . . 4
⊢ (𝑑 = 𝐷 → (〈𝐵, 𝑑〉Cgr〈𝑓, ℎ〉 ↔ 〈𝐵, 𝐷〉Cgr〈𝑓, ℎ〉)) |
| 33 | 30, 32 | anbi12d 632 |
. . 3
⊢ (𝑑 = 𝐷 → ((〈𝐴, 𝑑〉Cgr〈𝑒, ℎ〉 ∧ 〈𝐵, 𝑑〉Cgr〈𝑓, ℎ〉) ↔ (〈𝐴, 𝐷〉Cgr〈𝑒, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝑓, ℎ〉))) |
| 34 | 33 | 3anbi3d 1444 |
. 2
⊢ (𝑑 = 𝐷 → (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝑓, 𝑔〉) ∧ (〈𝐴, 𝑑〉Cgr〈𝑒, ℎ〉 ∧ 〈𝐵, 𝑑〉Cgr〈𝑓, ℎ〉)) ↔ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝑓, 𝑔〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝑒, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝑓, ℎ〉)))) |
| 35 | | opeq1 4873 |
. . . . 5
⊢ (𝑒 = 𝐸 → 〈𝑒, 𝑔〉 = 〈𝐸, 𝑔〉) |
| 36 | 35 | breq2d 5155 |
. . . 4
⊢ (𝑒 = 𝐸 → (𝑓 Btwn 〈𝑒, 𝑔〉 ↔ 𝑓 Btwn 〈𝐸, 𝑔〉)) |
| 37 | 36 | anbi2d 630 |
. . 3
⊢ (𝑒 = 𝐸 → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ↔ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝑓 Btwn 〈𝐸, 𝑔〉))) |
| 38 | | opeq1 4873 |
. . . . 5
⊢ (𝑒 = 𝐸 → 〈𝑒, 𝑓〉 = 〈𝐸, 𝑓〉) |
| 39 | 38 | breq2d 5155 |
. . . 4
⊢ (𝑒 = 𝐸 → (〈𝐴, 𝐵〉Cgr〈𝑒, 𝑓〉 ↔ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑓〉)) |
| 40 | 39 | anbi1d 631 |
. . 3
⊢ (𝑒 = 𝐸 → ((〈𝐴, 𝐵〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝑓, 𝑔〉) ↔ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝑓〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝑓, 𝑔〉))) |
| 41 | | opeq1 4873 |
. . . . 5
⊢ (𝑒 = 𝐸 → 〈𝑒, ℎ〉 = 〈𝐸, ℎ〉) |
| 42 | 41 | breq2d 5155 |
. . . 4
⊢ (𝑒 = 𝐸 → (〈𝐴, 𝐷〉Cgr〈𝑒, ℎ〉 ↔ 〈𝐴, 𝐷〉Cgr〈𝐸, ℎ〉)) |
| 43 | 42 | anbi1d 631 |
. . 3
⊢ (𝑒 = 𝐸 → ((〈𝐴, 𝐷〉Cgr〈𝑒, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝑓, ℎ〉) ↔ (〈𝐴, 𝐷〉Cgr〈𝐸, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝑓, ℎ〉))) |
| 44 | 37, 40, 43 | 3anbi123d 1438 |
. 2
⊢ (𝑒 = 𝐸 → (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝑓, 𝑔〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝑒, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝑓, ℎ〉)) ↔ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝑓 Btwn 〈𝐸, 𝑔〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝑓〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝑓, 𝑔〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝑓, ℎ〉)))) |
| 45 | | breq1 5146 |
. . . 4
⊢ (𝑓 = 𝐹 → (𝑓 Btwn 〈𝐸, 𝑔〉 ↔ 𝐹 Btwn 〈𝐸, 𝑔〉)) |
| 46 | 45 | anbi2d 630 |
. . 3
⊢ (𝑓 = 𝐹 → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝑓 Btwn 〈𝐸, 𝑔〉) ↔ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝑔〉))) |
| 47 | | opeq2 4874 |
. . . . 5
⊢ (𝑓 = 𝐹 → 〈𝐸, 𝑓〉 = 〈𝐸, 𝐹〉) |
| 48 | 47 | breq2d 5155 |
. . . 4
⊢ (𝑓 = 𝐹 → (〈𝐴, 𝐵〉Cgr〈𝐸, 𝑓〉 ↔ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉)) |
| 49 | | opeq1 4873 |
. . . . 5
⊢ (𝑓 = 𝐹 → 〈𝑓, 𝑔〉 = 〈𝐹, 𝑔〉) |
| 50 | 49 | breq2d 5155 |
. . . 4
⊢ (𝑓 = 𝐹 → (〈𝐵, 𝐶〉Cgr〈𝑓, 𝑔〉 ↔ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝑔〉)) |
| 51 | 48, 50 | anbi12d 632 |
. . 3
⊢ (𝑓 = 𝐹 → ((〈𝐴, 𝐵〉Cgr〈𝐸, 𝑓〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝑓, 𝑔〉) ↔ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝑔〉))) |
| 52 | | opeq1 4873 |
. . . . 5
⊢ (𝑓 = 𝐹 → 〈𝑓, ℎ〉 = 〈𝐹, ℎ〉) |
| 53 | 52 | breq2d 5155 |
. . . 4
⊢ (𝑓 = 𝐹 → (〈𝐵, 𝐷〉Cgr〈𝑓, ℎ〉 ↔ 〈𝐵, 𝐷〉Cgr〈𝐹, ℎ〉)) |
| 54 | 53 | anbi2d 630 |
. . 3
⊢ (𝑓 = 𝐹 → ((〈𝐴, 𝐷〉Cgr〈𝐸, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝑓, ℎ〉) ↔ (〈𝐴, 𝐷〉Cgr〈𝐸, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, ℎ〉))) |
| 55 | 46, 51, 54 | 3anbi123d 1438 |
. 2
⊢ (𝑓 = 𝐹 → (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝑓 Btwn 〈𝐸, 𝑔〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝑓〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝑓, 𝑔〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝑓, ℎ〉)) ↔ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝑔〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝑔〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, ℎ〉)))) |
| 56 | | opeq2 4874 |
. . . . 5
⊢ (𝑔 = 𝐺 → 〈𝐸, 𝑔〉 = 〈𝐸, 𝐺〉) |
| 57 | 56 | breq2d 5155 |
. . . 4
⊢ (𝑔 = 𝐺 → (𝐹 Btwn 〈𝐸, 𝑔〉 ↔ 𝐹 Btwn 〈𝐸, 𝐺〉)) |
| 58 | 57 | anbi2d 630 |
. . 3
⊢ (𝑔 = 𝐺 → ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝑔〉) ↔ (𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉))) |
| 59 | | opeq2 4874 |
. . . . 5
⊢ (𝑔 = 𝐺 → 〈𝐹, 𝑔〉 = 〈𝐹, 𝐺〉) |
| 60 | 59 | breq2d 5155 |
. . . 4
⊢ (𝑔 = 𝐺 → (〈𝐵, 𝐶〉Cgr〈𝐹, 𝑔〉 ↔ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉)) |
| 61 | 60 | anbi2d 630 |
. . 3
⊢ (𝑔 = 𝐺 → ((〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝑔〉) ↔ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉))) |
| 62 | 58, 61 | 3anbi12d 1439 |
. 2
⊢ (𝑔 = 𝐺 → (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝑔〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝑔〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, ℎ〉)) ↔ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, ℎ〉)))) |
| 63 | | opeq2 4874 |
. . . . 5
⊢ (ℎ = 𝐻 → 〈𝐸, ℎ〉 = 〈𝐸, 𝐻〉) |
| 64 | 63 | breq2d 5155 |
. . . 4
⊢ (ℎ = 𝐻 → (〈𝐴, 𝐷〉Cgr〈𝐸, ℎ〉 ↔ 〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉)) |
| 65 | | opeq2 4874 |
. . . . 5
⊢ (ℎ = 𝐻 → 〈𝐹, ℎ〉 = 〈𝐹, 𝐻〉) |
| 66 | 65 | breq2d 5155 |
. . . 4
⊢ (ℎ = 𝐻 → (〈𝐵, 𝐷〉Cgr〈𝐹, ℎ〉 ↔ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)) |
| 67 | 64, 66 | anbi12d 632 |
. . 3
⊢ (ℎ = 𝐻 → ((〈𝐴, 𝐷〉Cgr〈𝐸, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, ℎ〉) ↔ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉))) |
| 68 | 67 | 3anbi3d 1444 |
. 2
⊢ (ℎ = 𝐻 → (((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, ℎ〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, ℎ〉)) ↔ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)))) |
| 69 | | fveq2 6906 |
. 2
⊢ (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁)) |
| 70 | | df-ofs 35984 |
. 2
⊢
OuterFiveSeg = {〈𝑝,
𝑞〉 ∣
∃𝑛 ∈ ℕ
∃𝑎 ∈
(𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)∃𝑔 ∈ (𝔼‘𝑛)∃ℎ ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑓 Btwn 〈𝑒, 𝑔〉) ∧ (〈𝑎, 𝑏〉Cgr〈𝑒, 𝑓〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑓, 𝑔〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑒, ℎ〉 ∧ 〈𝑏, 𝑑〉Cgr〈𝑓, ℎ〉)))} |
| 71 | 10, 21, 28, 34, 44, 55, 62, 68, 69, 70 | br8 35756 |
1
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 OuterFiveSeg 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ ((𝐵 Btwn 〈𝐴, 𝐶〉 ∧ 𝐹 Btwn 〈𝐸, 𝐺〉) ∧ (〈𝐴, 𝐵〉Cgr〈𝐸, 𝐹〉 ∧ 〈𝐵, 𝐶〉Cgr〈𝐹, 𝐺〉) ∧ (〈𝐴, 𝐷〉Cgr〈𝐸, 𝐻〉 ∧ 〈𝐵, 𝐷〉Cgr〈𝐹, 𝐻〉)))) |