| Step | Hyp | Ref
| Expression |
| 1 | | simprll 779 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → 𝑦 Btwn 〈𝐶, 𝐷〉) |
| 2 | | simprrr 782 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) |
| 3 | 1, 2 | jca 511 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)) |
| 4 | | simpl1 1192 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 5 | | simpl23 1254 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 6 | | simprl 771 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝑦 ∈ (𝔼‘𝑁)) |
| 7 | | simpl31 1255 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
| 8 | | simpl32 1256 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁)) |
| 9 | | simprr 773 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝑧 ∈ (𝔼‘𝑁)) |
| 10 | | cgrxfr 36056 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉))) |
| 11 | 4, 5, 6, 7, 8, 9, 10 | syl132anc 1390 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉))) |
| 12 | 11 | adantr 480 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉))) |
| 13 | 3, 12 | mpd 15 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉)) |
| 14 | | anass 468 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ 𝑤 ∈ (𝔼‘𝑁)) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ ((𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁)) ∧ 𝑤 ∈ (𝔼‘𝑁)))) |
| 15 | | df-3an 1089 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁)) ↔ ((𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁)) ∧ 𝑤 ∈ (𝔼‘𝑁))) |
| 16 | 15 | anbi2i 623 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ ((𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁)) ∧ 𝑤 ∈ (𝔼‘𝑁)))) |
| 17 | 14, 16 | bitr4i 278 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ 𝑤 ∈ (𝔼‘𝑁)) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁)))) |
| 18 | | simpl1 1192 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 19 | | simpl23 1254 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 20 | | simpr1 1195 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝑦 ∈ (𝔼‘𝑁)) |
| 21 | | simpl31 1255 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
| 22 | | simpl32 1256 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁)) |
| 23 | | simpr3 1197 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝑤 ∈ (𝔼‘𝑁)) |
| 24 | | simpr2 1196 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝑧 ∈ (𝔼‘𝑁)) |
| 25 | | brcgr3 36047 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉 ↔ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉))) |
| 26 | 18, 19, 20, 21, 22, 23, 24, 25 | syl133anc 1395 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉 ↔ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉))) |
| 27 | 26 | anbi2d 630 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → ((𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉) ↔ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) |
| 28 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ((𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉) ↔ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) |
| 29 | | df-3an 1089 |
. . . . . . . . . . 11
⊢ (((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉))) ↔ (((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) |
| 30 | | simpl33 1257 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁)) |
| 31 | | simpr3l 1235 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → 𝑤 Btwn 〈𝐸, 𝑧〉) |
| 32 | | simpr2l 1233 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → 𝑧 Btwn 〈𝐸, 𝐹〉) |
| 33 | 18, 22, 23, 24, 30, 31, 32 | btwnexchand 36027 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → 𝑤 Btwn 〈𝐸, 𝐹〉) |
| 34 | | simpl21 1252 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 35 | | simpl22 1253 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
| 36 | | simpr1r 1232 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) |
| 37 | | simp3r1 1282 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉))) → 〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉) |
| 38 | 37 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → 〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉) |
| 39 | 18, 34, 35, 19, 20, 22, 23, 36, 38 | cgrtrand 35994 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉) |
| 40 | 33, 39 | jca 511 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → (𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉)) |
| 41 | 29, 40 | sylan2br 595 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ (((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → (𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉)) |
| 42 | 41 | expr 456 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ((𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)) → (𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
| 43 | 28, 42 | sylbid 240 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ((𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉) → (𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
| 44 | 17, 43 | sylanb 581 |
. . . . . . 7
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝐹 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
𝑤 ∈
(𝔼‘𝑁)) ∧
((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ((𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉) → (𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
| 45 | 44 | an32s 652 |
. . . . . 6
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝐹 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) ∧ 𝑤 ∈ (𝔼‘𝑁)) → ((𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉) → (𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
| 46 | 45 | reximdva 3168 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → (∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
| 47 | 13, 46 | mpd 15 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉)) |
| 48 | 47 | exp31 419 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁)) → (((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉)))) |
| 49 | 48 | rexlimdvv 3212 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
| 50 | | simp1 1137 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
| 51 | | simp21 1207 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
| 52 | | simp22 1208 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
| 53 | | simp23 1209 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
| 54 | | simp31 1210 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
| 55 | | brsegle 36109 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 56 | 50, 51, 52, 53, 54, 55 | syl122anc 1381 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
| 57 | | simp32 1211 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁)) |
| 58 | | simp33 1212 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁)) |
| 59 | | brsegle 36109 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉 ↔ ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) |
| 60 | 50, 53, 54, 57, 58, 59 | syl122anc 1381 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉 ↔ ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) |
| 61 | 56, 60 | anbi12d 632 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉) ↔ (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)))) |
| 62 | | reeanv 3229 |
. . 3
⊢
(∃𝑦 ∈
(𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)) ↔ (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) |
| 63 | 61, 62 | bitr4di 289 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)))) |
| 64 | | brsegle 36109 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐸, 𝐹〉 ↔ ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
| 65 | 50, 51, 52, 57, 58, 64 | syl122anc 1381 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐸, 𝐹〉 ↔ ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
| 66 | 49, 63, 65 | 3imtr4d 294 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉) → 〈𝐴, 𝐵〉 Seg≤ 〈𝐸, 𝐹〉)) |