Step | Hyp | Ref
| Expression |
1 | | simprll 802 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → 𝑦 Btwn 〈𝐶, 𝐷〉) |
2 | | simprrr 805 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) |
3 | 1, 2 | jca 554 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → (𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)) |
4 | | simpl1 1064 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
5 | | simpl23 1141 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
6 | | simprl 794 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝑦 ∈ (𝔼‘𝑁)) |
7 | | simpl31 1142 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
8 | | simpl32 1143 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁)) |
9 | | simprr 796 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → 𝑧 ∈ (𝔼‘𝑁)) |
10 | | cgrxfr 32162 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉))) |
11 | 4, 5, 6, 7, 8, 9, 10 | syl132anc 1344 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉))) |
12 | 11 | adantr 481 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉))) |
13 | 3, 12 | mpd 15 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉)) |
14 | | anass 681 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ 𝑤 ∈ (𝔼‘𝑁)) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ ((𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁)) ∧ 𝑤 ∈ (𝔼‘𝑁)))) |
15 | | df-3an 1039 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁)) ↔ ((𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁)) ∧ 𝑤 ∈ (𝔼‘𝑁))) |
16 | 15 | anbi2i 730 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ ((𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁)) ∧ 𝑤 ∈ (𝔼‘𝑁)))) |
17 | 14, 16 | bitr4i 267 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ 𝑤 ∈ (𝔼‘𝑁)) ↔ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁)))) |
18 | | simpl1 1064 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
19 | | simpl23 1141 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
20 | | simpr1 1067 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝑦 ∈ (𝔼‘𝑁)) |
21 | | simpl31 1142 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
22 | | simpl32 1143 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁)) |
23 | | simpr3 1069 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝑤 ∈ (𝔼‘𝑁)) |
24 | | simpr2 1068 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝑧 ∈ (𝔼‘𝑁)) |
25 | | brcgr3 32153 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑦 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉 ↔ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉))) |
26 | 18, 19, 20, 21, 22, 23, 24, 25 | syl133anc 1349 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → (〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉 ↔ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉))) |
27 | 26 | anbi2d 740 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → ((𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉) ↔ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) |
28 | 27 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ((𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉) ↔ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) |
29 | | df-3an 1039 |
. . . . . . . . . . 11
⊢ (((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉))) ↔ (((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) |
30 | | simpl33 1144 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁)) |
31 | | simpr3l 1122 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → 𝑤 Btwn 〈𝐸, 𝑧〉) |
32 | | simpr2l 1120 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → 𝑧 Btwn 〈𝐸, 𝐹〉) |
33 | 18, 22, 23, 24, 30, 31, 32 | btwnexchand 32133 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → 𝑤 Btwn 〈𝐸, 𝐹〉) |
34 | | simpl21 1139 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
35 | | simpl22 1140 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
36 | | simpr1r 1119 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) |
37 | | simp3r1 1169 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉))) → 〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉) |
38 | 37 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → 〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉) |
39 | 18, 34, 35, 19, 20, 22, 23, 36, 38 | cgrtrand 32100 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉) |
40 | 33, 39 | jca 554 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → (𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉)) |
41 | 29, 40 | sylan2br 493 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ (((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)) ∧ (𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)))) → (𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉)) |
42 | 41 | expr 643 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ((𝑤 Btwn 〈𝐸, 𝑧〉 ∧ (〈𝐶, 𝑦〉Cgr〈𝐸, 𝑤〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉 ∧ 〈𝑦, 𝐷〉Cgr〈𝑤, 𝑧〉)) → (𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
43 | 28, 42 | sylbid 230 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁) ∧ 𝑤 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ((𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉) → (𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
44 | 17, 43 | sylanb 489 |
. . . . . . 7
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝐹 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
𝑤 ∈
(𝔼‘𝑁)) ∧
((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ((𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉) → (𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
45 | 44 | an32s 846 |
. . . . . 6
⊢
(((((𝑁 ∈
ℕ ∧ (𝐴 ∈
(𝔼‘𝑁) ∧
𝐵 ∈
(𝔼‘𝑁) ∧
𝐶 ∈
(𝔼‘𝑁)) ∧
(𝐷 ∈
(𝔼‘𝑁) ∧
𝐸 ∈
(𝔼‘𝑁) ∧
𝐹 ∈
(𝔼‘𝑁))) ∧
(𝑦 ∈
(𝔼‘𝑁) ∧
𝑧 ∈
(𝔼‘𝑁))) ∧
((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) ∧ 𝑤 ∈ (𝔼‘𝑁)) → ((𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉) → (𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
46 | 45 | reximdva 3017 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → (∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝑧〉 ∧ 〈𝐶, 〈𝑦, 𝐷〉〉Cgr3〈𝐸, 〈𝑤, 𝑧〉〉) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
47 | 13, 46 | mpd 15 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) ∧ (𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁))) ∧ ((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉)) |
48 | 47 | exp31 630 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((𝑦 ∈ (𝔼‘𝑁) ∧ 𝑧 ∈ (𝔼‘𝑁)) → (((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉)))) |
49 | 48 | rexlimdvv 3037 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)) → ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
50 | | simp1 1061 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝑁 ∈ ℕ) |
51 | | simp21 1094 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁)) |
52 | | simp22 1095 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁)) |
53 | | simp23 1096 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁)) |
54 | | simp31 1097 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁)) |
55 | | brsegle 32215 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
56 | 50, 51, 52, 53, 54, 55 | syl122anc 1335 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ↔ ∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉))) |
57 | | simp32 1098 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁)) |
58 | | simp33 1099 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → 𝐹 ∈ (𝔼‘𝑁)) |
59 | | brsegle 32215 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉 ↔ ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) |
60 | 50, 53, 54, 57, 58, 59 | syl122anc 1335 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉 ↔ ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) |
61 | 56, 60 | anbi12d 747 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉) ↔ (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)))) |
62 | | reeanv 3107 |
. . 3
⊢
(∃𝑦 ∈
(𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)) ↔ (∃𝑦 ∈ (𝔼‘𝑁)(𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ ∃𝑧 ∈ (𝔼‘𝑁)(𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉))) |
63 | 61, 62 | syl6bbr 278 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑦 Btwn 〈𝐶, 𝐷〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐶, 𝑦〉) ∧ (𝑧 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐶, 𝐷〉Cgr〈𝐸, 𝑧〉)))) |
64 | | brsegle 32215 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐸, 𝐹〉 ↔ ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
65 | 50, 51, 52, 57, 58, 64 | syl122anc 1335 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → (〈𝐴, 𝐵〉 Seg≤ 〈𝐸, 𝐹〉 ↔ ∃𝑤 ∈ (𝔼‘𝑁)(𝑤 Btwn 〈𝐸, 𝐹〉 ∧ 〈𝐴, 𝐵〉Cgr〈𝐸, 𝑤〉))) |
66 | 49, 63, 65 | 3imtr4d 283 |
1
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐹 ∈ (𝔼‘𝑁))) → ((〈𝐴, 𝐵〉 Seg≤ 〈𝐶, 𝐷〉 ∧ 〈𝐶, 𝐷〉 Seg≤ 〈𝐸, 𝐹〉) → 〈𝐴, 𝐵〉 Seg≤ 〈𝐸, 𝐹〉)) |