Metamath Proof Explorer

Theorem btwnconn1lem14

Description: Lemma for btwnconn1 . Final statement of the theorem when B =/= C . (Contributed by Scott Fenton, 9-Oct-2013)

Ref Expression
Assertion btwnconn1lem14 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D → C Btwn A D ∨ D Btwn A C

Proof

Step Hyp Ref Expression
1 simp1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → N ∈ ℕ
2 simp2l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
3 simp3r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
4 simp3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N
5 axsegcon ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → ∃ c ∈ 𝔼 ⁡ N D Btwn A c ∧ D c Cgr C D
6 1 2 3 4 5 syl121anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → ∃ c ∈ 𝔼 ⁡ N D Btwn A c ∧ D c Cgr C D
7 simp3l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
8 axsegcon ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → ∃ d ∈ 𝔼 ⁡ N C Btwn A d ∧ C d Cgr C D
9 1 2 7 4 8 syl121anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → ∃ d ∈ 𝔼 ⁡ N C Btwn A d ∧ C d Cgr C D
10 reeanv ⊢ ∃ c ∈ 𝔼 ⁡ N ∃ d ∈ 𝔼 ⁡ N D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ↔ ∃ c ∈ 𝔼 ⁡ N D Btwn A c ∧ D c Cgr C D ∧ ∃ d ∈ 𝔼 ⁡ N C Btwn A d ∧ C d Cgr C D
11 6 9 10 sylanbrc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → ∃ c ∈ 𝔼 ⁡ N ∃ d ∈ 𝔼 ⁡ N D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D
12 11 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D → ∃ c ∈ 𝔼 ⁡ N ∃ d ∈ 𝔼 ⁡ N D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D
13 simpl1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → N ∈ ℕ
14 simpl2l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
15 simprl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → c ∈ 𝔼 ⁡ N
16 simpl3l ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
17 simpl2r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
18 axsegcon ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∃ b ∈ 𝔼 ⁡ N c Btwn A b ∧ c b Cgr C B
19 13 14 15 16 17 18 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → ∃ b ∈ 𝔼 ⁡ N c Btwn A b ∧ c b Cgr C B
20 simprr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → d ∈ 𝔼 ⁡ N
21 simpl3r ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → D ∈ 𝔼 ⁡ N
22 axsegcon ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∃ x ∈ 𝔼 ⁡ N d Btwn A x ∧ d x Cgr D B
23 13 14 20 21 17 22 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → ∃ x ∈ 𝔼 ⁡ N d Btwn A x ∧ d x Cgr D B
24 19 23 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → ∃ b ∈ 𝔼 ⁡ N c Btwn A b ∧ c b Cgr C B ∧ ∃ x ∈ 𝔼 ⁡ N d Btwn A x ∧ d x Cgr D B
25 24 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → ∃ b ∈ 𝔼 ⁡ N c Btwn A b ∧ c b Cgr C B ∧ ∃ x ∈ 𝔼 ⁡ N d Btwn A x ∧ d x Cgr D B
26 reeanv ⊢ ∃ b ∈ 𝔼 ⁡ N ∃ x ∈ 𝔼 ⁡ N c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B ↔ ∃ b ∈ 𝔼 ⁡ N c Btwn A b ∧ c b Cgr C B ∧ ∃ x ∈ 𝔼 ⁡ N d Btwn A x ∧ d x Cgr D B
27 25 26 sylibr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → ∃ b ∈ 𝔼 ⁡ N ∃ x ∈ 𝔼 ⁡ N c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B
28 13 14 17 3jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N
29 28 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N
30 16 21 15 3jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N
31 30 adantr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N
32 simplrr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → d ∈ 𝔼 ⁡ N
33 simprl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → b ∈ 𝔼 ⁡ N
34 simprr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → x ∈ 𝔼 ⁡ N
35 32 33 34 3jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N
36 29 31 35 3jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N
37 simpll ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B → A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D
38 simplr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B → D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D
39 simpr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B → c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B
40 37 38 39 3jca ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B → A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B
41 btwnconn1lem2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B → x = b
42 36 40 41 syl2an ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B → x = b
43 opeq2 ⊢ x = b → A x = A b
44 43 breq2d ⊢ x = b → d Btwn A x ↔ d Btwn A b
45 opeq2 ⊢ x = b → d x = d b
46 45 breq1d ⊢ x = b → d x Cgr D B ↔ d b Cgr D B
47 44 46 anbi12d ⊢ x = b → d Btwn A x ∧ d x Cgr D B ↔ d Btwn A b ∧ d b Cgr D B
48 47 anbi2d ⊢ x = b → c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B ↔ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B
49 48 anbi2d ⊢ x = b → A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B ↔ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B
50 49 biimpac ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B ∧ x = b → A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B
51 32 33 jca ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N
52 29 31 51 jca32 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N
53 simpll ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D
54 simplr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D
55 simpr ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B
56 53 54 55 3jca ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B
57 btwnconn1lem13 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → C = c ∨ D = d
58 52 56 57 syl2an ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → C = c ∨ D = d
59 58 ex ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A b ∧ d b Cgr D B → C = c ∨ D = d
60 50 59 syl5 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B ∧ x = b → C = c ∨ D = d
61 60 expdimp ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B → x = b → C = c ∨ D = d
62 42 61 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B → C = c ∨ D = d
63 62 an4s ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D ∧ b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B → C = c ∨ D = d
64 63 exp32 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → b ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B → C = c ∨ D = d
65 64 rexlimdvv ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → ∃ b ∈ 𝔼 ⁡ N ∃ x ∈ 𝔼 ⁡ N c Btwn A b ∧ c b Cgr C B ∧ d Btwn A x ∧ d x Cgr D B → C = c ∨ D = d
66 27 65 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → C = c ∨ D = d
67 orcom ⊢ C = c ∨ D = d ↔ D = d ∨ C = c
68 simprrl ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → C Btwn A d
69 68 adantl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → C Btwn A d
70 opeq2 ⊢ D = d → A D = A d
71 70 breq2d ⊢ D = d → C Btwn A D ↔ C Btwn A d
72 69 71 syl5ibrcom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → D = d → C Btwn A D
73 simprll ⊢ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → D Btwn A c
74 73 adantl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → D Btwn A c
75 opeq2 ⊢ C = c → A C = A c
76 75 breq2d ⊢ C = c → D Btwn A C ↔ D Btwn A c
77 74 76 syl5ibrcom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → C = c → D Btwn A C
78 72 77 orim12d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → D = d ∨ C = c → C Btwn A D ∨ D Btwn A C
79 67 78 syl5bi ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → C = c ∨ D = d → C Btwn A D ∨ D Btwn A C
80 66 79 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → C Btwn A D ∨ D Btwn A C
81 80 an4s ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D ∧ c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N ∧ D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → C Btwn A D ∨ D Btwn A C
82 81 exp32 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D → c ∈ 𝔼 ⁡ N ∧ d ∈ 𝔼 ⁡ N → D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → C Btwn A D ∨ D Btwn A C
83 82 rexlimdvv ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D → ∃ c ∈ 𝔼 ⁡ N ∃ d ∈ 𝔼 ⁡ N D Btwn A c ∧ D c Cgr C D ∧ C Btwn A d ∧ C d Cgr C D → C Btwn A D ∨ D Btwn A C
84 12 83 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ B ≠ C ∧ B Btwn A C ∧ B Btwn A D → C Btwn A D ∨ D Btwn A C