Metamath Proof Explorer

Theorem btwnswapid

Description: If you can swap the first two arguments of a betweenness statement, then those arguments are identical. Theorem 3.4 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

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

Proof

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