Metamath Proof Explorer

Theorem btwncomim

Description: Betweenness commutes. Implication version. Theorem 3.2 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion btwncomim ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Btwn B C → A Btwn C B

Proof

Step Hyp Ref Expression
1 btwntriv2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → C Btwn A C
2 1 3adant3r2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → C Btwn A C
3 simpl ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → N ∈ ℕ
4 simpr2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
5 simpr1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
6 simpr3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → C ∈ 𝔼 ⁡ N
7 axpasch ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Btwn B C ∧ C Btwn A C → ∃ x ∈ 𝔼 ⁡ N x Btwn A A ∧ x Btwn C B
8 3 4 5 6 5 6 7 syl132anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Btwn B C ∧ C Btwn A C → ∃ x ∈ 𝔼 ⁡ N x Btwn A A ∧ x Btwn C B
9 2 8 mpan2d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Btwn B C → ∃ x ∈ 𝔼 ⁡ N x Btwn A A ∧ x Btwn C B
10 simpll ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → N ∈ ℕ
11 simpr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → x ∈ 𝔼 ⁡ N
12 simplr1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
13 axbtwnid ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → x Btwn A A → x = A
14 10 11 12 13 syl3anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → x Btwn A A → x = A
15 breq1 ⊢ x = A → x Btwn C B ↔ A Btwn C B
16 15 biimpd ⊢ x = A → x Btwn C B → A Btwn C B
17 14 16 syl6 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → x Btwn A A → x Btwn C B → A Btwn C B
18 17 impd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → x Btwn A A ∧ x Btwn C B → A Btwn C B
19 18 rexlimdva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → ∃ x ∈ 𝔼 ⁡ N x Btwn A A ∧ x Btwn C B → A Btwn C B
20 9 19 syld ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Btwn B C → A Btwn C B