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 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
2 simpr2 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simpr1 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
4 simpr3 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
5 axpasch ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐴 , 𝐴 ⟩ ∧ 𝑥 Btwn ⟨ 𝐵 , 𝐵 ⟩ ) ) )
6 1 2 3 4 3 2 5 syl132anc ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐴 , 𝐴 ⟩ ∧ 𝑥 Btwn ⟨ 𝐵 , 𝐵 ⟩ ) ) )
7 simpll ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
8 simpr ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
9 simplr1 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
10 axbtwnid ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝐴 , 𝐴 ⟩ → 𝑥 = 𝐴 ) )
11 7 8 9 10 syl3anc ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝐴 , 𝐴 ⟩ → 𝑥 = 𝐴 ) )
12 simplr2 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
13 axbtwnid ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝐵 , 𝐵 ⟩ → 𝑥 = 𝐵 ) )
14 7 8 12 13 syl3anc ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝐵 , 𝐵 ⟩ → 𝑥 = 𝐵 ) )
15 11 14 anim12d ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑥 Btwn ⟨ 𝐴 , 𝐴 ⟩ ∧ 𝑥 Btwn ⟨ 𝐵 , 𝐵 ⟩ ) → ( 𝑥 = 𝐴𝑥 = 𝐵 ) ) )
16 eqtr2 ( ( 𝑥 = 𝐴𝑥 = 𝐵 ) → 𝐴 = 𝐵 )
17 15 16 syl6 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑥 Btwn ⟨ 𝐴 , 𝐴 ⟩ ∧ 𝑥 Btwn ⟨ 𝐵 , 𝐵 ⟩ ) → 𝐴 = 𝐵 ) )
18 17 rexlimdva ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐴 , 𝐴 ⟩ ∧ 𝑥 Btwn ⟨ 𝐵 , 𝐵 ⟩ ) → 𝐴 = 𝐵 ) )
19 6 18 syld ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) → 𝐴 = 𝐵 ) )