Metamath Proof Explorer

Theorem btwntriv2

Description: Betweenness always holds for the second endpoint. Theorem 3.1 of Schwabhauser p. 30. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion btwntriv2 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐵 ⟩ )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
2 simp2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
3 simp3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
4 axsegcon ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ) )
5 1 2 3 3 3 4 syl122anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ) )
6 simpl1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
7 simpl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
8 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
9 axcgrid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ → 𝐵 = 𝑥 ) )
10 6 7 8 7 9 syl13anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ → 𝐵 = 𝑥 ) )
11 opeq2 ⊢ ( 𝐵 = 𝑥 → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑥 ⟩ )
12 11 breq2d ⊢ ( 𝐵 = 𝑥 → ( 𝐵 Btwn ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) )
13 12 biimprd ⊢ ( 𝐵 = 𝑥 → ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ → 𝐵 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )
14 10 13 syl6 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ → ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ → 𝐵 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) )
15 14 impd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )
16 15 ancomsd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )
17 16 rexlimdva ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐵 , 𝐵 ⟩ ) → 𝐵 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )
18 5 17 mpd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 Btwn ⟨ 𝐴 , 𝐵 ⟩ )