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 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B Btwn A B

Proof

Step Hyp Ref Expression
1 simp1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → N ∈ ℕ
2 simp2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
3 simp3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
4 axsegcon ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∃ x ∈ 𝔼 ⁡ N B Btwn A x ∧ B x Cgr B B
5 1 2 3 3 3 4 syl122anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∃ x ∈ 𝔼 ⁡ N B Btwn A x ∧ B x Cgr B B
6 simpl1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → N ∈ ℕ
7 simpl3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
8 simpr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → x ∈ 𝔼 ⁡ N
9 axcgrid ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B x Cgr B B → B = x
10 6 7 8 7 9 syl13anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → B x Cgr B B → B = x
11 opeq2 ⊢ B = x → A B = A x
12 11 breq2d ⊢ B = x → B Btwn A B ↔ B Btwn A x
13 12 biimprd ⊢ B = x → B Btwn A x → B Btwn A B
14 10 13 syl6 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → B x Cgr B B → B Btwn A x → B Btwn A B
15 14 impd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → B x Cgr B B ∧ B Btwn A x → B Btwn A B
16 15 ancomsd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ x ∈ 𝔼 ⁡ N → B Btwn A x ∧ B x Cgr B B → B Btwn A B
17 16 rexlimdva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → ∃ x ∈ 𝔼 ⁡ N B Btwn A x ∧ B x Cgr B B → B Btwn A B
18 5 17 mpd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B Btwn A B